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.
27 lines
907 B
Plaintext
27 lines
907 B
Plaintext
/**
|
|
* Checks that within a basic block, if a node is annotated then its
|
|
* successor is also annotated (or excluded). A gap in annotations
|
|
* within a basic block indicates a missing annotation, since there
|
|
* are no branches to justify the gap.
|
|
*
|
|
* Nodes with exceptional successors are excluded, as the exception
|
|
* edge leaves the basic block and the normal successor may be dead.
|
|
*/
|
|
|
|
import python
|
|
import TimerUtils
|
|
|
|
from TimerCfgNode a, ControlFlowNode succ
|
|
where
|
|
exists(BasicBlock bb, int i |
|
|
a = bb.getNode(i) and
|
|
succ = bb.getNode(i + 1)
|
|
) and
|
|
not succ instanceof TimerCfgNode and
|
|
not isUnannotatable(succ.getNode()) and
|
|
not isTimerMechanism(succ.getNode(), a.getTestFunction()) and
|
|
not exists(a.getAnExceptionalSuccessor()) and
|
|
succ.getNode() instanceof Expr
|
|
select a, "Annotated node followed by unannotated $@ in the same basic block", succ,
|
|
succ.getNode().toString()
|