Skip to content

Commit 73b3e02

Browse files
committed
C++: Add a small library for control-flow reachability.
1 parent 651cc04 commit 73b3e02

File tree

1 file changed

+62
-0
lines changed

1 file changed

+62
-0
lines changed

cpp/ql/src/Likely Bugs/Leap Year/UncheckedReturnValueForTimeFunctions.ql

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,68 @@
1414
import cpp
1515
import LeapYear
1616

17+
signature module InputSig {
18+
predicate isSource(ControlFlowNode n);
19+
20+
predicate isSink(ControlFlowNode n);
21+
}
22+
23+
module ControlFlowReachability<InputSig Input> {
24+
pragma[nomagic]
25+
private predicate fwd(ControlFlowNode n) {
26+
Input::isSource(n)
27+
or
28+
exists(ControlFlowNode n0 |
29+
fwd(n0) and
30+
n0.getASuccessor() = n
31+
)
32+
}
33+
34+
pragma[nomagic]
35+
private predicate rev(ControlFlowNode n) {
36+
fwd(n) and
37+
(
38+
Input::isSink(n)
39+
or
40+
exists(ControlFlowNode n1 |
41+
rev(n1) and
42+
n.getASuccessor() = n1
43+
)
44+
)
45+
}
46+
47+
pragma[nomagic]
48+
private predicate prunedSuccessor(ControlFlowNode n1, ControlFlowNode n2) {
49+
rev(n1) and
50+
rev(n2) and
51+
n1.getASuccessor() = n2
52+
}
53+
54+
pragma[nomagic]
55+
predicate isSource(ControlFlowNode n) {
56+
Input::isSource(n) and
57+
rev(n)
58+
}
59+
60+
pragma[nomagic]
61+
predicate isSink(ControlFlowNode n) {
62+
Input::isSink(n) and
63+
rev(n)
64+
}
65+
66+
pragma[nomagic]
67+
private predicate successorPlus(ControlFlowNode n1, ControlFlowNode n2) =
68+
doublyBoundedFastTC(prunedSuccessor/2, isSource/1, isSink/1)(n1, n2)
69+
70+
predicate flowsTo(ControlFlowNode n1, ControlFlowNode n2) {
71+
successorPlus(n1, n2)
72+
or
73+
n1 = n2 and
74+
isSource(n1) and
75+
isSink(n2)
76+
}
77+
}
78+
1779
from FunctionCall fcall, TimeConversionFunction trf, Variable var
1880
where
1981
fcall = trf.getACallToThisFunction() and

0 commit comments

Comments
 (0)