@@ -27,8 +27,12 @@ predicate blockContainsPreprocessorBranches(BasicBlock bb) {
27
27
)
28
28
}
29
29
30
- from GuardCondition gc , FreeCall fc , Variable v , BasicBlock bb
31
- where
30
+ /**
31
+ * Holds if `gc` ensures that `v` is non-zero when reaching `bb`, and `bb`
32
+ * contains a single statement which is `fc`.
33
+ */
34
+ pragma [ nomagic]
35
+ private predicate interesting ( GuardCondition gc , FreeCall fc , Variable v , BasicBlock bb ) {
32
36
gc .ensuresEq ( v .getAnAccess ( ) , 0 , bb , false ) and
33
37
fc .getArgument ( 0 ) = v .getAnAccess ( ) and
34
38
bb = fc .getBasicBlock ( ) and
39
43
// Block statement with a single nested statement: if (x) { free(x); }
40
44
strictcount ( bb .( BlockStmt ) .getAStmt ( ) ) = 1
41
45
) and
42
- strictcount ( BasicBlock bb2 | gc .ensuresEq ( _, 0 , bb2 , _) | bb2 ) = 1 and
43
46
not fc .isInMacroExpansion ( ) and
44
47
not blockContainsPreprocessorBranches ( bb ) and
45
48
not ( gc instanceof BinaryOperation and not gc instanceof ComparisonOperation ) and
46
49
not exists ( CommaExpr c | c .getAChild * ( ) = fc )
50
+ }
51
+
52
+ /** Holds if `gc` only guards a single block. */
53
+ bindingset [ gc]
54
+ pragma [ inline_late]
55
+ private predicate guardConditionGuardsUniqueBlock ( GuardCondition gc ) {
56
+ strictcount ( BasicBlock bb | gc .ensuresEq ( _, 0 , bb , _) ) = 1
57
+ }
58
+
59
+ from GuardCondition gc , FreeCall fc , Variable v , BasicBlock bb
60
+ where
61
+ interesting ( gc , fc , v , bb ) and
62
+ guardConditionGuardsUniqueBlock ( gc )
47
63
select gc , "unnecessary NULL check before call to $@" , fc , "free"
0 commit comments