@@ -23,18 +23,26 @@ predicate candidateForStmt(ForStmt forStmt, Variable v, CrementOperation update,
2323 rel = forStmt .getCondition ( )
2424}
2525
26- predicate illDefinedDecrForStmt ( ForStmt forstmt , Variable v , Expr initialCondition , Expr terminalCondition ) {
27- exists ( DecrementOperation dec , RelationalOperation rel |
28- // decrementing for loop
29- candidateForStmt ( forstmt , v , dec , rel ) and
26+ pragma [ noinline ]
27+ predicate candidateDecrForStmt ( ForStmt forStmt , Variable v , VariableAccess lesserOperand , Expr terminalCondition ) {
28+ exists ( DecrementOperation update , RelationalOperation rel |
29+ candidateForStmt ( forStmt , v , update , rel ) and
3030
3131 // condition is `v < terminalCondition`
3232 terminalCondition = rel .getGreaterOperand ( ) and
33- v .getAnAccess ( ) = rel .getLesserOperand ( ) and
33+ lesserOperand = rel .getLesserOperand ( ) and
34+ v .getAnAccess ( ) = lesserOperand
35+ )
36+ }
37+
38+ predicate illDefinedDecrForStmt ( ForStmt forstmt , Variable v , Expr initialCondition , Expr terminalCondition ) {
39+ exists ( VariableAccess lesserOperand |
40+ // decrementing for loop
41+ candidateDecrForStmt ( forstmt , v , lesserOperand , terminalCondition ) and
3442
3543 // `initialCondition` is a value of `v` in the for loop
3644 v .getAnAssignedValue ( ) = initialCondition and
37- DataFlow:: localFlowStep ( DataFlow:: exprNode ( initialCondition ) , DataFlow:: exprNode ( rel . getLesserOperand ( ) ) ) and
45+ DataFlow:: localFlowStep ( DataFlow:: exprNode ( initialCondition ) , DataFlow:: exprNode ( lesserOperand ) ) and
3846
3947 // `initialCondition` < `terminalCondition`
4048 (
@@ -45,18 +53,26 @@ predicate illDefinedDecrForStmt( ForStmt forstmt, Variable v, Expr initialCondit
4553 )
4654}
4755
48- predicate illDefinedIncrForStmt ( ForStmt forstmt , Variable v , Expr initialCondition , Expr terminalCondition ) {
49- exists ( IncrementOperation inc , RelationalOperation rel |
50- // incrementing for loop
51- candidateForStmt ( forstmt , v , inc , rel ) and
56+ pragma [ noinline ]
57+ predicate candidateIncrForStmt ( ForStmt forStmt , Variable v , VariableAccess greaterOperand , Expr terminalCondition ) {
58+ exists ( IncrementOperation update , RelationalOperation rel |
59+ candidateForStmt ( forStmt , v , update , rel ) and
5260
5361 // condition is `v > terminalCondition`
5462 terminalCondition = rel .getLesserOperand ( ) and
55- v .getAnAccess ( ) = rel .getGreaterOperand ( ) and
63+ greaterOperand = rel .getGreaterOperand ( ) and
64+ v .getAnAccess ( ) = greaterOperand
65+ )
66+ }
67+
68+ predicate illDefinedIncrForStmt ( ForStmt forstmt , Variable v , Expr initialCondition , Expr terminalCondition ) {
69+ exists ( VariableAccess greaterOperand |
70+ // incrementing for loop
71+ candidateIncrForStmt ( forstmt , v , greaterOperand , terminalCondition ) and
5672
5773 // `initialCondition` is a value of `v` in the for loop
5874 v .getAnAssignedValue ( ) = initialCondition and
59- DataFlow:: localFlowStep ( DataFlow:: exprNode ( initialCondition ) , DataFlow:: exprNode ( rel . getGreaterOperand ( ) ) ) and
75+ DataFlow:: localFlowStep ( DataFlow:: exprNode ( initialCondition ) , DataFlow:: exprNode ( greaterOperand ) ) and
6076
6177 // `terminalCondition` < `initialCondition`
6278 (
0 commit comments