@@ -115,30 +115,29 @@ predicate pointerDereference(CatchAnyBlock cb, Variable vr, Variable vro) {
115
115
/** Holds if `vro` may be released in the `catch`. */
116
116
pragma [ inline]
117
117
predicate newThrowDelete ( CatchAnyBlock cb , Variable vro ) {
118
- exists ( Expr e0 , AssignExpr ase , NewOrNewArrayExpr nae |
118
+ exists ( Expr e0 , AssignExpr ase , NewOrNewArrayExpr nae |
119
119
ase = vro .getAnAccess ( ) .getEnclosingStmt ( ) .( ExprStmt ) .getExpr ( ) .( AssignExpr ) and
120
120
nae = ase .getRValue ( ) .( NewOrNewArrayExpr ) and
121
121
not nae .getAChild * ( ) .toString ( ) = "nothrow" and
122
- (
123
- e0 = nae or
124
- e0 = nae .getEnclosingFunction ( ) .getACallToThisFunction ( )
125
- ) and
126
- vro = ase .getLValue ( ) .( VariableAccess ) .getTarget ( ) and
127
- e0 .getEnclosingStmt ( ) .getParentStmt * ( ) = cb .getTryStmt ( ) .getStmt ( ) and
122
+ (
123
+ e0 = nae or
124
+ e0 = nae .getEnclosingFunction ( ) .getACallToThisFunction ( )
125
+ ) and
126
+ vro = ase .getLValue ( ) .( VariableAccess ) .getTarget ( ) and
127
+ e0 .getEnclosingStmt ( ) .getParentStmt * ( ) = cb .getTryStmt ( ) .getStmt ( ) and
128
128
not exists ( AssignExpr ase1 |
129
129
vro = ase1 .getLValue ( ) .( VariableAccess ) .getTarget ( ) and
130
130
ase1 .getRValue ( ) .getValue ( ) = "0" and
131
131
ase1 .getASuccessor * ( ) = e0
132
132
)
133
133
) and
134
- not exists ( Initializer it |
134
+ not exists ( Initializer it |
135
135
vro .getInitializer ( ) = it and
136
- it .getExpr ( ) .getValue ( ) = "0"
136
+ it .getExpr ( ) .getValue ( ) = "0"
137
137
) and
138
- not exists ( ConstructorFieldInit ci |
139
- vro = ci .getTarget ( )
140
- )
138
+ not exists ( ConstructorFieldInit ci | vro = ci .getTarget ( ) )
141
139
}
140
+
142
141
from CatchAnyBlock cb , string msg
143
142
where
144
143
exists ( Variable vr , Variable vro , Expr exp |
@@ -185,14 +184,16 @@ where
185
184
exists ( Variable vro , Expr exp |
186
185
exp .getEnclosingStmt ( ) .getParentStmt * ( ) = cb and
187
186
exists ( VariableAccess va |
188
- (
189
- va = exp .( DeleteArrayExpr ) .getExpr ( ) .( VariableAccess ) or
190
- va = exp .( DeleteExpr ) .getExpr ( ) .( VariableAccess )
191
- ) and
192
- va .getEnclosingStmt ( ) = exp .getEnclosingStmt ( ) and
193
- vro = va .getTarget ( )
187
+ (
188
+ va = exp .( DeleteArrayExpr ) .getExpr ( ) .( VariableAccess ) or
189
+ va = exp .( DeleteExpr ) .getExpr ( ) .( VariableAccess )
190
+ ) and
191
+ va .getEnclosingStmt ( ) = exp .getEnclosingStmt ( ) and
192
+ vro = va .getTarget ( )
194
193
) and
195
- newThrowDelete ( cb , vro ) and
196
- msg = "If the allocation in the try block fails, then an unallocated pointer " + vro .getName ( ) + " will be freed in the catch block."
194
+ newThrowDelete ( cb , vro ) and
195
+ msg =
196
+ "If the allocation in the try block fails, then an unallocated pointer " + vro .getName ( ) +
197
+ " will be freed in the catch block."
197
198
)
198
199
select cb , msg
0 commit comments