1313
1414import cpp
1515
16- /** Holds if the release can occur twice. in the current block of catch and above in the block of try or other block catch . */
16+ /** Holds if `vr` may be released in the `try` block associated with `cb`, or in a `catch` block prior to `cb` . */
1717pragma [ inline]
1818predicate doubleCallDelete ( CatchAnyBlock cb , Variable vr ) {
1919 // Search for exceptions after freeing memory.
2020 exists ( Expr e1 |
21+ // `e1` is a delete of `vr`
2122 (
2223 e1 = vr .getAnAccess ( ) .getEnclosingStmt ( ) .( ExprStmt ) .getExpr ( ) .( DeleteArrayExpr ) or
2324 e1 = vr .getAnAccess ( ) .getEnclosingStmt ( ) .( ExprStmt ) .getExpr ( ) .( DeleteExpr )
2425 ) and
2526 e1 .getEnclosingFunction ( ) = cb .getEnclosingFunction ( ) and
2627 (
28+ // `e1` occurs in the `try` block associated with `cb`
2729 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`
2831 exists ( Expr e2 , ThrowExpr th |
2932 (
3033 e2 = th or
@@ -33,6 +36,7 @@ predicate doubleCallDelete(CatchAnyBlock cb, Variable vr) {
3336 e2 .getEnclosingStmt ( ) .getParentStmt * ( ) = cb .getTryStmt ( ) .getStmt ( ) and
3437 e1 .getASuccessor + ( ) = e2
3538 ) and
39+ // there is no assignment `vr = 0` in the `try` block after `e1`
3640 not exists ( AssignExpr ae |
3741 ae .getLValue ( ) .( VariableAccess ) .getTarget ( ) = vr and
3842 ae .getRValue ( ) .getValue ( ) = "0" and
@@ -44,12 +48,14 @@ predicate doubleCallDelete(CatchAnyBlock cb, Variable vr) {
4448 exists ( CatchBlock cbt , Expr e2 , ThrowExpr th |
4549 e1 .getEnclosingStmt ( ) .getParentStmt * ( ) = cbt and
4650 exists ( cbt .getParameter ( ) ) and
51+ // `e2` is a `throw` (or a function call that may throw) that occurs in the `catch` block after `e1`
4752 (
4853 e2 = th or
4954 e2 = th .getEnclosingFunction ( ) .getACallToThisFunction ( )
5055 ) and
5156 e2 .getEnclosingStmt ( ) .getParentStmt * ( ) = cbt and
5257 e1 .getASuccessor + ( ) = e2 and
58+ // there is no assignment `vr = 0` in the `catch` block after `e1`
5359 not exists ( AssignExpr ae |
5460 ae .getLValue ( ) .( VariableAccess ) .getTarget ( ) = vr and
5561 ae .getRValue ( ) .getValue ( ) = "0" and
@@ -71,6 +77,7 @@ predicate pointerDereference(CatchAnyBlock cb, Variable vr, Variable vro) {
7177 // Search exceptions before allocating memory.
7278 exists ( Expr e0 , Expr e1 |
7379 (
80+ // `e0` is a `new` expression (or equivalent function call) assigned to `vro`
7481 exists ( AssignExpr ase |
7582 ase = vro .getAnAccess ( ) .getEnclosingStmt ( ) .( ExprStmt ) .getExpr ( ) .( AssignExpr ) and
7683 (
@@ -90,6 +97,7 @@ predicate pointerDereference(CatchAnyBlock cb, Variable vr, Variable vro) {
9097 vro = ase .getLValue ( ) .getAPredecessor ( ) .( VariableAccess ) .getTarget ( )
9198 )
9299 ) and
100+ // `e1` is a `new` expression (or equivalent function call) assigned to `vr`
93101 exists ( AssignExpr ase |
94102 ase = vr .getAnAccess ( ) .getEnclosingStmt ( ) .( ExprStmt ) .getExpr ( ) .( AssignExpr ) and
95103 (
@@ -101,6 +109,7 @@ predicate pointerDereference(CatchAnyBlock cb, Variable vr, Variable vro) {
101109 e0 .getASuccessor * ( ) = e1 and
102110 e0 .getEnclosingStmt ( ) .getParentStmt * ( ) = cb .getTryStmt ( ) .getStmt ( ) and
103111 e1 .getEnclosingStmt ( ) .getParentStmt * ( ) = cb .getTryStmt ( ) .getStmt ( ) and
112+ // `e2` is a `throw` (or a function call that may throw) that occurs in the `try` block before `e0`
104113 exists ( Expr e2 , ThrowExpr th |
105114 (
106115 e2 = th or
@@ -159,7 +168,7 @@ where
159168 ) and
160169 doubleCallDelete ( cb , vr ) and
161170 msg =
162- "perhaps a situation of uncertainty due to the repeated call of the delete function for the variable "
171+ "This allocation may have been released in the try block or a previous catch block. "
163172 + vr .getName ( )
164173 )
165174select cb , msg
0 commit comments