@@ -15,7 +15,7 @@ import cpp
1515
1616/** Holds if `vr` may be released in the `try` block associated with `cb`, or in a `catch` block prior to `cb`. */
1717pragma [ inline]
18- predicate doubleCallDelete ( CatchAnyBlock cb , Variable vr ) {
18+ predicate doubleCallDelete ( BlockStmt b , CatchAnyBlock cb , Variable vr ) {
1919 // Search for exceptions after freeing memory.
2020 exists ( Expr e1 |
2121 // `e1` is a delete of `vr`
@@ -24,50 +24,32 @@ predicate doubleCallDelete(CatchAnyBlock cb, Variable vr) {
2424 e1 = vr .getAnAccess ( ) .getEnclosingStmt ( ) .( ExprStmt ) .getExpr ( ) .( DeleteExpr )
2525 ) and
2626 e1 .getEnclosingFunction ( ) = cb .getEnclosingFunction ( ) and
27- (
28- // `e1` occurs in the `try` block associated with `cb`
29- e1 .getEnclosingStmt ( ) .getParentStmt * ( ) = cb .getTryStmt ( ) .getStmt ( ) and
30- // `e2` is a `throw` (or a function call that may throw) that occurs in the `try` block after `e1`
31- exists ( Expr e2 , ThrowExpr th |
32- (
33- e2 = th or
34- e2 = th .getEnclosingFunction ( ) .getACallToThisFunction ( )
35- ) and
36- e2 .getEnclosingStmt ( ) .getParentStmt * ( ) = cb .getTryStmt ( ) .getStmt ( ) and
37- e1 .getASuccessor + ( ) = e2
27+ // there is no assignment `vr = 0` in the `try` block after `e1`
28+ not exists ( AssignExpr ae |
29+ ae .getLValue ( ) .( VariableAccess ) .getTarget ( ) = vr and
30+ ae .getRValue ( ) .getValue ( ) = "0" and
31+ e1 .getASuccessor + ( ) = ae and
32+ ae .getEnclosingStmt ( ) .getParentStmt * ( ) = b
33+ ) and
34+ // `e2` is a `throw` (or a function call that may throw) that occurs in the `try` or `catch` block after `e1`
35+ exists ( Expr e2 , ThrowExpr th |
36+ (
37+ e2 = th or
38+ e2 = th .getEnclosingFunction ( ) .getACallToThisFunction ( )
3839 ) and
39- // there is no assignment `vr = 0` in the `try` block after `e1`
40- not exists ( AssignExpr ae |
41- ae . getLValue ( ) . ( VariableAccess ) . getTarget ( ) = vr and
42- ae . getRValue ( ) .getValue ( ) = "0" and
43- e1 . getASuccessor + ( ) = ae and
44- ae . getEnclosingStmt ( ) . getParentStmt * ( ) = cb . getTryStmt ( ) . getStmt ( )
45- )
40+ e2 . getEnclosingStmt ( ) . getParentStmt * ( ) = b and
41+ e1 . getASuccessor + ( ) = e2
42+ ) and
43+ e1 . getEnclosingStmt ( ) .getParentStmt * ( ) = b and
44+ (
45+ // Search for a situation where there is a release in the block of `try`.
46+ b = cb . getTryStmt ( ) . getStmt ( )
4647 or
4748 // Search for a situation when there is a higher catch block that also frees memory.
48- exists ( CatchBlock cbt , Expr e2 , ThrowExpr th |
49- e1 .getEnclosingStmt ( ) .getParentStmt * ( ) = cbt and
50- exists ( cbt .getParameter ( ) ) and
51- // `e2` is a `throw` (or a function call that may throw) that occurs in the `catch` block after `e1`
52- (
53- e2 = th or
54- e2 = th .getEnclosingFunction ( ) .getACallToThisFunction ( )
55- ) and
56- e2 .getEnclosingStmt ( ) .getParentStmt * ( ) = cbt and
57- e1 .getASuccessor + ( ) = e2 and
58- // there is no assignment `vr = 0` in the `catch` block after `e1`
59- not exists ( AssignExpr ae |
60- ae .getLValue ( ) .( VariableAccess ) .getTarget ( ) = vr and
61- ae .getRValue ( ) .getValue ( ) = "0" and
62- e1 .getASuccessor + ( ) = ae and
63- ae .getEnclosingStmt ( ) .getParentStmt * ( ) = cbt
64- )
65- )
49+ exists ( b .( CatchBlock ) .getParameter ( ) )
6650 ) and
6751 // Exclude the presence of a check in catch block.
68- not exists ( IfStmt ifst |
69- ifst .getEnclosingStmt ( ) .getParentStmt * ( ) = cb .getAStmt ( )
70- )
52+ not exists ( IfStmt ifst | ifst .getEnclosingStmt ( ) .getParentStmt * ( ) = cb .getAStmt ( ) )
7153 )
7254}
7355
@@ -166,9 +148,9 @@ where
166148 exp .( DeleteArrayExpr ) .getEnclosingStmt ( ) .getParentStmt * ( ) = cb and
167149 vr = exp .( DeleteArrayExpr ) .getExpr ( ) .( VariableAccess ) .getTarget ( )
168150 ) and
169- doubleCallDelete ( cb , vr ) and
151+ doubleCallDelete ( _ , cb , vr ) and
170152 msg =
171- "This allocation may have been released in the try block or a previous catch block."
172- + vr .getName ( )
153+ "This allocation may have been released in the try block or a previous catch block." +
154+ vr .getName ( )
173155 )
174156select cb , msg
0 commit comments