mirror of
https://github.com/github/codeql.git
synced 2026-05-14 11:19:27 +02:00
These use the annotated, self-verifying test files to check various consistency requirements. Some of these may be expressing the same thing in different ways, but it's fairly cheap to keep them around, so I have not attempted to produce a minimal set of queries for this.
26 lines
952 B
Plaintext
26 lines
952 B
Plaintext
/**
|
|
* Stronger version of NoBackwardFlow: for consecutive annotated nodes
|
|
* A -> B that both have a single timestamp (non-loop code) and B does
|
|
* NOT dominate A (forward edge), requires max(A) < min(B).
|
|
*/
|
|
|
|
import python
|
|
import TimerUtils
|
|
|
|
from TimerCfgNode a, TimerCfgNode b, int maxA, int minB
|
|
where
|
|
nextTimerAnnotation(a, b) and
|
|
not a.isDead() and
|
|
not b.isDead() and
|
|
// Only apply to non-loop code (single timestamps on both sides)
|
|
strictcount(a.getATimestamp()) = 1 and
|
|
strictcount(b.getATimestamp()) = 1 and
|
|
// Forward edge: B does not strictly dominate A (excludes loop back-edges
|
|
// but still checks same-basic-block pairs)
|
|
not b.getBasicBlock().strictlyDominates(a.getBasicBlock()) and
|
|
maxA = max(a.getATimestamp()) and
|
|
minB = min(b.getATimestamp()) and
|
|
maxA >= minB
|
|
select a, "Strict forward violation: $@ flows to $@", a.getTimestampExpr(maxA), "timestamp " + maxA,
|
|
b.getTimestampExpr(minB), "timestamp " + minB
|