@@ -32,7 +32,7 @@ class CallMayNotReturn extends FunctionCall {
3232
3333/** Holds if there are no assignment expressions to the function argument. */
3434pragma [ inline]
35- predicate checkChangeVariable ( FunctionCall fc0 , FunctionCall fc1 , FunctionCall fc2 ) {
35+ predicate checkChangeVariable ( FunctionCall fc0 , ControlFlowNode fc1 , ControlFlowNode fc2 ) {
3636 not exists ( Expr exptmp |
3737 (
3838 exptmp = fc0 .getArgument ( 0 ) .( VariableAccess ) .getTarget ( ) .getAnAssignedValue ( ) or
@@ -76,83 +76,13 @@ predicate checkChangeVariable(FunctionCall fc0, FunctionCall fc1, FunctionCall f
7676/** Holds if the underlying expression is a call to the close function. Provided that the function parameter does not change after the call. */
7777predicate closeReturn ( FunctionCall fc ) {
7878 fcloseCall ( fc , _) and
79- not exists ( Expr exptmp |
80- (
81- exptmp = fc .getArgument ( 0 ) .( VariableAccess ) .getTarget ( ) .getAnAssignedValue ( ) or
82- exptmp .( AddressOfExpr ) .getOperand ( ) =
83- fc .getArgument ( 0 ) .( VariableAccess ) .getTarget ( ) .getAnAccess ( )
84- ) and
85- exptmp = fc .getASuccessor * ( )
86- ) and
87- (
88- (
89- not fc .getArgument ( 0 ) instanceof PointerFieldAccess and
90- not fc .getArgument ( 0 ) instanceof ValueFieldAccess
91- or
92- fc .getArgument ( 0 ) .( VariableAccess ) .getQualifier ( ) instanceof ThisExpr
93- )
94- or
95- not exists ( Expr exptmp |
96- (
97- exptmp =
98- fc .getArgument ( 0 )
99- .( VariableAccess )
100- .getQualifier ( )
101- .( VariableAccess )
102- .getTarget ( )
103- .getAnAssignedValue ( ) or
104- exptmp .( AddressOfExpr ) .getOperand ( ) =
105- fc .getArgument ( 0 )
106- .( VariableAccess )
107- .getQualifier ( )
108- .( VariableAccess )
109- .getTarget ( )
110- .getAnAccess ( )
111- ) and
112- exptmp = fc .getASuccessor * ( )
113- )
114- )
79+ checkChangeVariable ( fc , fc , fc .getEnclosingFunction ( ) )
11580}
11681
11782/** Holds if the underlying expression is a call to the close function. Provided that the function parameter does not change before the call. */
11883predicate closeWithoutChangeBefore ( FunctionCall fc ) {
11984 fcloseCall ( fc , _) and
120- not exists ( Expr exptmp |
121- (
122- exptmp = fc .getArgument ( 0 ) .( VariableAccess ) .getTarget ( ) .getAnAssignedValue ( ) or
123- exptmp .( AddressOfExpr ) .getOperand ( ) =
124- fc .getArgument ( 0 ) .( VariableAccess ) .getTarget ( ) .getAnAccess ( )
125- ) and
126- exptmp = fc .getAPredecessor * ( )
127- ) and
128- (
129- (
130- not fc .getArgument ( 0 ) instanceof PointerFieldAccess and
131- not fc .getArgument ( 0 ) instanceof ValueFieldAccess
132- or
133- fc .getArgument ( 0 ) .( VariableAccess ) .getQualifier ( ) instanceof ThisExpr
134- )
135- or
136- not exists ( Expr exptmp |
137- (
138- exptmp =
139- fc .getArgument ( 0 )
140- .( VariableAccess )
141- .getQualifier ( )
142- .( VariableAccess )
143- .getTarget ( )
144- .getAnAssignedValue ( ) or
145- exptmp .( AddressOfExpr ) .getOperand ( ) =
146- fc .getArgument ( 0 )
147- .( VariableAccess )
148- .getQualifier ( )
149- .( VariableAccess )
150- .getTarget ( )
151- .getAnAccess ( )
152- ) and
153- exptmp = fc .getAPredecessor * ( )
154- )
155- )
85+ checkChangeVariable ( fc , fc .getEnclosingFunction ( ) .getEntryPoint ( ) , fc )
15686}
15787
15888/** Holds, if a sequential call of the specified functions is possible, via a higher-level function call. */
@@ -205,7 +135,7 @@ where
205135 closeWithoutChangeBefore ( fc1 ) and
206136 callInOtherFunctions ( fc , fc1 )
207137 or
208- // detection of repeated call in different functions
138+ // detection of repeated call in different functions
209139 interDoubleCloseFunctions ( fc , fc1 )
210140 ) and
211141 similarArguments ( fc , fc1 )
0 commit comments