@@ -72,14 +72,14 @@ Expr getLoopStepOfForStmt(ForStmt forLoop) {
72
72
* Holds if the given function has as parameter at a given index a pointer to a
73
73
* constant value or a reference of a constant value.
74
74
*/
75
- predicate functionHasConstPointerOrReferenceParameter ( Function function , int index ) {
75
+ private predicate functionHasConstPointerOrReferenceParameter ( Function function , int index ) {
76
76
function .getParameter ( index ) .getType ( ) .( PointerType ) .getBaseType ( ) .isConst ( ) or
77
77
function .getParameter ( index ) .getType ( ) .( ReferenceType ) .getBaseType ( ) .isConst ( )
78
78
}
79
79
80
80
/**
81
81
* Holds if the the variable behind a given variable access is taken its address
82
- * in a declaration in either the body of the for-loop or in its update expression .
82
+ * in a non-const variable declaration, in the body of the for-loop.
83
83
*
84
84
* e.g.1. The loop counter variable `i` in the body is taken its address in the
85
85
* declaration of a pointer variable `m`.
@@ -96,13 +96,21 @@ predicate functionHasConstPointerOrReferenceParameter(Function function, int ind
96
96
* }
97
97
* ```
98
98
*/
99
- predicate variableAddressTakenInDeclaration ( ForStmt forLoop , VariableAccess baseVariableAccess ) {
99
+ predicate variableAddressTakenInNonConstDeclaration (
100
+ ForStmt forLoop , VariableAccess baseVariableAccess
101
+ ) {
100
102
exists ( AddressOfExpr addressOfExpr , DeclStmt decl |
101
103
decl .getParentStmt + ( ) = forLoop and
102
104
decl .getADeclarationEntry ( ) .( VariableDeclarationEntry ) .getVariable ( ) .getInitializer ( ) .getExpr ( ) =
103
105
addressOfExpr and
104
- baseVariableAccess .getTarget ( ) =
105
- forLoop .getCondition ( ) .( LegacyForLoopCondition ) .getLoopBound ( ) .( VariableAccess ) .getTarget ( )
106
+ addressOfExpr .getOperand ( ) = baseVariableAccess and
107
+ not decl .getADeclarationEntry ( )
108
+ .( VariableDeclarationEntry )
109
+ .getVariable ( )
110
+ .getType ( )
111
+ .( PointerType )
112
+ .getBaseType ( )
113
+ .isConst ( )
106
114
)
107
115
}
108
116
@@ -126,14 +134,15 @@ predicate variableAddressTakenInDeclaration(ForStmt forLoop, VariableAccess base
126
134
* }
127
135
* ```
128
136
*/
129
- predicate variableAddressTakenAsConstArgument (
137
+ private predicate variableAddressTakenAsConstArgument (
130
138
ForStmt forLoop , VariableAccess baseVariableAccess , Call call
131
139
) {
132
140
exists ( AddressOfExpr addressOfExpr , int index |
133
- call .getParent + ( ) = forLoop .getAChild + ( ) and
141
+ call .getParent + ( ) = forLoop .getAChild + ( ) and // TODO: Bad
134
142
call .getArgument ( index ) .getAChild * ( ) = addressOfExpr and
135
143
functionHasConstPointerOrReferenceParameter ( call .getTarget ( ) , index ) and
136
- addressOfExpr .getOperand ( ) = baseVariableAccess .getTarget ( ) .getAnAccess ( )
144
+ addressOfExpr .getOperand ( ) = baseVariableAccess .getTarget ( ) .getAnAccess ( ) and
145
+ baseVariableAccess .getParent + ( ) = forLoop
137
146
)
138
147
}
139
148
@@ -152,11 +161,11 @@ predicate variableAddressTakenAsConstArgument(
152
161
*/
153
162
predicate variableAddressTakenInExpression ( ForStmt forLoop , VariableAccess baseVariableAccess ) {
154
163
exists ( AddressOfExpr addressOfExpr |
155
- baseVariableAccess .getParent + ( ) = forLoop .getAChild + ( ) and
164
+ baseVariableAccess .getParent + ( ) = forLoop .getAChild + ( ) and // TODO: Bad
156
165
addressOfExpr .getParent + ( ) = forLoop .getAChild + ( ) and
157
166
addressOfExpr .getOperand ( ) = baseVariableAccess .getTarget ( ) .getAnAccess ( )
158
167
) and
159
- not exists ( Call call | variableAddressTakenAsConstArgument ( forLoop , baseVariableAccess , call ) )
168
+ not variableAddressTakenAsConstArgument ( forLoop , baseVariableAccess . getTarget ( ) . getAnAccess ( ) , _ )
160
169
}
161
170
162
171
from ForStmt forLoop
@@ -225,8 +234,17 @@ where
225
234
*/
226
235
227
236
/* 6-1. The loop counter is taken a mutable reference or its address to a mutable pointer. */
228
- variableAddressTakenInDeclaration ( forLoop ,
229
- forLoop .getCondition ( ) .( LegacyForLoopCondition ) .getLoopCounter ( ) )
237
+ exists ( VariableAccess loopCounterAccessInCondition |
238
+ loopCounterAccessInCondition = forLoop .getCondition ( ) .( LegacyForLoopCondition ) .getLoopCounter ( )
239
+ |
240
+ exists ( VariableAccess loopCounterAccessTakenAddress |
241
+ loopCounterAccessInCondition .getTarget ( ) = loopCounterAccessTakenAddress .getTarget ( )
242
+ |
243
+ variableAddressTakenInNonConstDeclaration ( forLoop , loopCounterAccessTakenAddress )
244
+ or
245
+ variableAddressTakenInExpression ( forLoop , loopCounterAccessTakenAddress )
246
+ )
247
+ )
230
248
or
231
249
/* 6-2. The loop bound is taken a mutable reference or its address to a mutable pointer. */
232
250
none ( )
0 commit comments