@@ -72,14 +72,14 @@ Expr getLoopStepOfForStmt(ForStmt forLoop) {
7272 * Holds if the given function has as parameter at a given index a pointer to a
7373 * constant value or a reference of a constant value.
7474 */
75- predicate functionHasConstPointerOrReferenceParameter ( Function function , int index ) {
75+ private predicate functionHasConstPointerOrReferenceParameter ( Function function , int index ) {
7676 function .getParameter ( index ) .getType ( ) .( PointerType ) .getBaseType ( ) .isConst ( ) or
7777 function .getParameter ( index ) .getType ( ) .( ReferenceType ) .getBaseType ( ) .isConst ( )
7878}
7979
8080/**
8181 * 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.
8383 *
8484 * e.g.1. The loop counter variable `i` in the body is taken its address in the
8585 * declaration of a pointer variable `m`.
@@ -96,13 +96,21 @@ predicate functionHasConstPointerOrReferenceParameter(Function function, int ind
9696 * }
9797 * ```
9898 */
99- predicate variableAddressTakenInDeclaration ( ForStmt forLoop , VariableAccess baseVariableAccess ) {
99+ predicate variableAddressTakenInNonConstDeclaration (
100+ ForStmt forLoop , VariableAccess baseVariableAccess
101+ ) {
100102 exists ( AddressOfExpr addressOfExpr , DeclStmt decl |
101103 decl .getParentStmt + ( ) = forLoop and
102104 decl .getADeclarationEntry ( ) .( VariableDeclarationEntry ) .getVariable ( ) .getInitializer ( ) .getExpr ( ) =
103105 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 ( )
106114 )
107115}
108116
@@ -126,14 +134,15 @@ predicate variableAddressTakenInDeclaration(ForStmt forLoop, VariableAccess base
126134 * }
127135 * ```
128136 */
129- predicate variableAddressTakenAsConstArgument (
137+ private predicate variableAddressTakenAsConstArgument (
130138 ForStmt forLoop , VariableAccess baseVariableAccess , Call call
131139) {
132140 exists ( AddressOfExpr addressOfExpr , int index |
133- call .getParent + ( ) = forLoop .getAChild + ( ) and
141+ call .getParent + ( ) = forLoop .getAChild + ( ) and // TODO: Bad
134142 call .getArgument ( index ) .getAChild * ( ) = addressOfExpr and
135143 functionHasConstPointerOrReferenceParameter ( call .getTarget ( ) , index ) and
136- addressOfExpr .getOperand ( ) = baseVariableAccess .getTarget ( ) .getAnAccess ( )
144+ addressOfExpr .getOperand ( ) = baseVariableAccess .getTarget ( ) .getAnAccess ( ) and
145+ baseVariableAccess .getParent + ( ) = forLoop
137146 )
138147}
139148
@@ -152,11 +161,11 @@ predicate variableAddressTakenAsConstArgument(
152161 */
153162predicate variableAddressTakenInExpression ( ForStmt forLoop , VariableAccess baseVariableAccess ) {
154163 exists ( AddressOfExpr addressOfExpr |
155- baseVariableAccess .getParent + ( ) = forLoop .getAChild + ( ) and
164+ baseVariableAccess .getParent + ( ) = forLoop .getAChild + ( ) and // TODO: Bad
156165 addressOfExpr .getParent + ( ) = forLoop .getAChild + ( ) and
157166 addressOfExpr .getOperand ( ) = baseVariableAccess .getTarget ( ) .getAnAccess ( )
158167 ) and
159- not exists ( Call call | variableAddressTakenAsConstArgument ( forLoop , baseVariableAccess , call ) )
168+ not variableAddressTakenAsConstArgument ( forLoop , baseVariableAccess . getTarget ( ) . getAnAccess ( ) , _ )
160169}
161170
162171from ForStmt forLoop
@@ -225,8 +234,17 @@ where
225234 */
226235
227236 /* 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+ )
230248 or
231249 /* 6-2. The loop bound is taken a mutable reference or its address to a mutable pointer. */
232250 none ( )
0 commit comments