@@ -27,8 +27,12 @@ predicate blockContainsPreprocessorBranches(BasicBlock bb) {
2727 )
2828}
2929
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 ) {
3236 gc .ensuresEq ( v .getAnAccess ( ) , 0 , bb , false ) and
3337 fc .getArgument ( 0 ) = v .getAnAccess ( ) and
3438 bb = fc .getBasicBlock ( ) and
3943 // Block statement with a single nested statement: if (x) { free(x); }
4044 strictcount ( bb .( BlockStmt ) .getAStmt ( ) ) = 1
4145 ) and
42- strictcount ( BasicBlock bb2 | gc .ensuresEq ( _, 0 , bb2 , _) | bb2 ) = 1 and
4346 not fc .isInMacroExpansion ( ) and
4447 not blockContainsPreprocessorBranches ( bb ) and
4548 not ( gc instanceof BinaryOperation and not gc instanceof ComparisonOperation ) and
4649 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 )
4763select gc , "unnecessary NULL check before call to $@" , fc , "free"
0 commit comments