@@ -189,28 +189,31 @@ predicate freedInSameMethod(Resource r, Expr acquire) {
189189 */
190190predicate leakedInSameMethod ( Resource r , Expr acquire ) {
191191 unreleasedResource ( r , acquire , _, _) and
192- (
193- exists ( FunctionCall fc |
194- // `r` (or something computed from it) is passed to another function
195- // near to where it's acquired, and might be stored elsewhere.
196- fc .getAnArgument ( ) .getAChild * ( ) = r .getAnAccess ( ) and
197- fc .getEnclosingFunction ( ) = acquire .getEnclosingFunction ( )
198- ) or exists ( Variable v , Expr e |
199- // `r` (or something computed from it) is stored in another variable
200- // near to where it's acquired, and might be released through that
201- // variable.
202- v .getAnAssignedValue ( ) = e and
203- e .getAChild * ( ) = r .getAnAccess ( ) and
204- e .getEnclosingFunction ( ) = acquire .getEnclosingFunction ( )
205- ) or exists ( FunctionCall fc |
206- // `this` (i.e. the class where `r` is acquired) is passed into `r` via a
207- // method, or the constructor. `r` may use this to register itself with
208- // `this` in some way, ensuring it is later deleted.
209- fc .getEnclosingFunction ( ) = acquire .getEnclosingFunction ( ) and
210- fc .getAnArgument ( ) instanceof ThisExpr and
211- (
212- fc .getQualifier ( ) = r .getAnAccess ( ) or // e.g. `r->setOwner(this)`
213- fc = acquire .getAChild * ( ) // e.g. `r = new MyClass(this)`
192+ exists ( Function f |
193+ acquire .getEnclosingFunction ( ) = f and
194+ (
195+ exists ( FunctionCall fc |
196+ // `r` (or something computed from it) is passed to another function
197+ // near to where it's acquired, and might be stored elsewhere.
198+ fc .getAnArgument ( ) .getAChild * ( ) = r .getAnAccess ( ) and
199+ fc .getEnclosingFunction ( ) = f
200+ ) or exists ( Variable v , Expr e |
201+ // `r` (or something computed from it) is stored in another variable
202+ // near to where it's acquired, and might be released through that
203+ // variable.
204+ v .getAnAssignedValue ( ) = e and
205+ e .getAChild * ( ) = r .getAnAccess ( ) and
206+ e .getEnclosingFunction ( ) = f
207+ ) or exists ( FunctionCall fc |
208+ // `this` (i.e. the class where `r` is acquired) is passed into `r` via a
209+ // method, or the constructor. `r` may use this to register itself with
210+ // `this` in some way, ensuring it is later deleted.
211+ fc .getEnclosingFunction ( ) = f and
212+ fc .getAnArgument ( ) instanceof ThisExpr and
213+ (
214+ fc .getQualifier ( ) = r .getAnAccess ( ) or // e.g. `r->setOwner(this)`
215+ fc = acquire .getAChild * ( ) // e.g. `r = new MyClass(this)`
216+ )
214217 )
215218 )
216219 )
0 commit comments