@@ -14,9 +14,9 @@ predicate allocated(FunctionCall fc) { allocExpr(fc, _) }
14
14
15
15
/** An expression for which there exists a function call that might free it. */
16
16
class FreedExpr extends PointsToExpr {
17
- FreedExpr ( ) { freeExprOrIndirect ( this , _ , _) }
17
+ FreedExpr ( ) { freeExprOrIndirect ( _ , this , _) }
18
18
19
- override predicate interesting ( ) { freeExprOrIndirect ( this , _ , _) }
19
+ override predicate interesting ( ) { freeExprOrIndirect ( _ , this , _) }
20
20
}
21
21
22
22
/**
@@ -59,19 +59,6 @@ predicate allocCallOrIndirect(Expr e) {
59
59
)
60
60
}
61
61
62
- predicate freeCallOrIndirect ( FunctionCall fc , Variable v ) {
63
- // direct free call
64
- v .getAnAccess ( ) = fc .( DeallocationExpr ) .getFreedExpr ( )
65
- or
66
- // indirect free call
67
- exists ( FunctionCall midcall , Function mid , int arg |
68
- fc .getArgument ( arg ) = v .getAnAccess ( ) and
69
- mayCallFunction ( fc , mid ) and
70
- midcall .getEnclosingFunction ( ) = mid and
71
- freeCallOrIndirect ( midcall , mid .getParameter ( arg ) )
72
- )
73
- }
74
-
75
62
predicate allocDefinition ( StackVariable v , ControlFlowNode def ) {
76
63
exists ( Expr expr | exprDefinition ( v , def , expr ) and allocCallOrIndirect ( expr ) )
77
64
}
@@ -86,7 +73,7 @@ class MallocVariableReachability extends StackVariableReachabilityWithReassignme
86
73
override predicate isSinkActual ( ControlFlowNode node , StackVariable v ) {
87
74
// node may be used in allocReaches
88
75
exists ( node .( AnalysedExpr ) .getNullSuccessor ( v ) ) or
89
- freeCallOrIndirect ( node , v ) or
76
+ freeExprOrIndirect ( node , v . getAnAccess ( ) , _ ) or
90
77
assignedToFieldOrGlobal ( v , node ) or
91
78
// node may be used directly in query
92
79
v .getFunction ( ) = node .( ReturnStmt ) .getEnclosingFunction ( )
@@ -133,7 +120,7 @@ class MallocReachability extends StackVariableReachabilityExt {
133
120
// assigned to a global at node, or NULL checked on the edge node -> next.
134
121
exists ( StackVariable v0 | mallocVariableReaches ( v0 , source , node ) |
135
122
node .( AnalysedExpr ) .getNullSuccessor ( v0 ) = next or
136
- freeCallOrIndirect ( node , v0 ) or
123
+ freeExprOrIndirect ( node , v0 . getAnAccess ( ) , _ ) or
137
124
assignedToFieldOrGlobal ( v0 , node )
138
125
)
139
126
}
0 commit comments