@@ -61,7 +61,7 @@ predicate pointerDereference(CatchAnyBlock cb, Variable vr, Variable vro) {
61
61
(
62
62
// `e0` is a `new` expression (or equivalent function call) assigned to `vro`
63
63
exists ( AssignExpr ase |
64
- ase = vro .getAnAccess ( ) .getEnclosingStmt ( ) .( ExprStmt ) .getExpr ( ) . ( AssignExpr ) and
64
+ ase = vro .getAnAccess ( ) .getEnclosingStmt ( ) .( ExprStmt ) .getExpr ( ) and
65
65
(
66
66
e0 = ase .getRValue ( ) .( NewOrNewArrayExpr ) or
67
67
e0 = ase .getRValue ( ) .( NewOrNewArrayExpr ) .getEnclosingFunction ( ) .getACallToThisFunction ( )
@@ -71,7 +71,7 @@ predicate pointerDereference(CatchAnyBlock cb, Variable vr, Variable vro) {
71
71
or
72
72
// `e0` is a `new` expression (or equivalent function call) assigned to the array element `vro`
73
73
exists ( AssignExpr ase |
74
- ase = vro .getAnAccess ( ) .( Qualifier ) .getEnclosingStmt ( ) .( ExprStmt ) .getExpr ( ) . ( AssignExpr ) and
74
+ ase = vro .getAnAccess ( ) .( Qualifier ) .getEnclosingStmt ( ) .( ExprStmt ) .getExpr ( ) and
75
75
(
76
76
e0 = ase .getRValue ( ) .( NewOrNewArrayExpr ) or
77
77
e0 = ase .getRValue ( ) .( NewOrNewArrayExpr ) .getEnclosingFunction ( ) .getACallToThisFunction ( )
@@ -82,7 +82,7 @@ predicate pointerDereference(CatchAnyBlock cb, Variable vr, Variable vro) {
82
82
) and
83
83
// `e1` is a `new` expression (or equivalent function call) assigned to `vr`
84
84
exists ( AssignExpr ase |
85
- ase = vr .getAnAccess ( ) .getEnclosingStmt ( ) .( ExprStmt ) .getExpr ( ) . ( AssignExpr ) and
85
+ ase = vr .getAnAccess ( ) .getEnclosingStmt ( ) .( ExprStmt ) .getExpr ( ) and
86
86
(
87
87
e1 = ase .getRValue ( ) .( NewOrNewArrayExpr ) or
88
88
e1 = ase .getRValue ( ) .( NewOrNewArrayExpr ) .getEnclosingFunction ( ) .getACallToThisFunction ( )
@@ -112,21 +112,48 @@ predicate pointerDereference(CatchAnyBlock cb, Variable vr, Variable vro) {
112
112
)
113
113
}
114
114
115
+ /** Holds if `vro` may be released in the `catch`. */
116
+ pragma [ inline]
117
+ predicate newThrowDelete ( CatchAnyBlock cb , Variable vro ) {
118
+ exists ( Expr e0 , AssignExpr ase , NewOrNewArrayExpr nae |
119
+ ase = vro .getAnAccess ( ) .getEnclosingStmt ( ) .( ExprStmt ) .getExpr ( ) .( AssignExpr ) and
120
+ nae = ase .getRValue ( ) .( NewOrNewArrayExpr ) and
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
128
+ not exists ( AssignExpr ase1 |
129
+ vro = ase1 .getLValue ( ) .( VariableAccess ) .getTarget ( ) and
130
+ ase1 .getRValue ( ) .getValue ( ) = "0" and
131
+ ase1 .getASuccessor * ( ) = e0
132
+ )
133
+ ) and
134
+ not exists ( Initializer it |
135
+ vro .getInitializer ( ) = it and
136
+ it .getExpr ( ) .getValue ( ) = "0"
137
+ ) and
138
+ not exists ( ConstructorFieldInit ci |
139
+ vro = ci .getTarget ( )
140
+ )
141
+ }
115
142
from CatchAnyBlock cb , string msg
116
143
where
117
144
exists ( Variable vr , Variable vro , Expr exp |
118
145
exp .getEnclosingStmt ( ) .getParentStmt * ( ) = cb and
119
146
exists ( VariableAccess va |
120
147
(
121
148
(
122
- va = exp .( DeleteArrayExpr ) .getExpr ( ) .getAPredecessor + ( ) .( Qualifier ) . ( VariableAccess ) or
123
- va = exp .( DeleteArrayExpr ) .getExpr ( ) .getAPredecessor + ( ) . ( VariableAccess )
149
+ va = exp .( DeleteArrayExpr ) .getExpr ( ) .getAPredecessor + ( ) .( Qualifier ) or
150
+ va = exp .( DeleteArrayExpr ) .getExpr ( ) .getAPredecessor + ( )
124
151
) and
125
152
vr = exp .( DeleteArrayExpr ) .getExpr ( ) .( VariableAccess ) .getTarget ( )
126
153
or
127
154
(
128
- va = exp .( DeleteExpr ) .getExpr ( ) .getAPredecessor + ( ) .( Qualifier ) . ( VariableAccess ) or
129
- va = exp .( DeleteExpr ) .getExpr ( ) .getAPredecessor + ( ) . ( VariableAccess )
155
+ va = exp .( DeleteExpr ) .getExpr ( ) .getAPredecessor + ( ) .( Qualifier ) or
156
+ va = exp .( DeleteExpr ) .getExpr ( ) .getAPredecessor + ( )
130
157
) and
131
158
vr = exp .( DeleteExpr ) .getExpr ( ) .( VariableAccess ) .getTarget ( )
132
159
) and
@@ -154,4 +181,18 @@ where
154
181
"This allocation may have been released in the try block or a previous catch block." +
155
182
vr .getName ( )
156
183
)
184
+ or
185
+ exists ( Variable vro , Expr exp |
186
+ exp .getEnclosingStmt ( ) .getParentStmt * ( ) = cb and
187
+ 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 ( )
194
+ ) 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."
197
+ )
157
198
select cb , msg
0 commit comments