@@ -62,7 +62,6 @@ predicate mayBeReturnZero(Function fn) {
62
62
}
63
63
64
64
/** Gets the Guard which compares the expression `bound` */
65
- pragma [ inline]
66
65
GuardCondition checkByValue ( Expr bound , Expr val ) {
67
66
exists ( GuardCondition gc |
68
67
(
@@ -122,6 +121,10 @@ predicate compareFunctionWithValue(Expr guardExp, Function compArg, Expr valArg)
122
121
pragma [ inline]
123
122
predicate checkConditions1 ( Expr div , Function fn , float changeInt ) {
124
123
exists ( Expr val |
124
+ (
125
+ val .getEnclosingFunction ( ) = fn or
126
+ val .getEnclosingFunction ( ) = div .getEnclosingFunction ( )
127
+ ) and
125
128
val .getValue ( ) .toFloat ( ) = changeInt and
126
129
compareFunctionWithValue ( div , fn , val )
127
130
)
@@ -169,6 +172,11 @@ predicate compareExprWithValue(Expr guardExp, Expr compArg, Expr valArg) {
169
172
pragma [ inline]
170
173
predicate checkConditions2 ( Expr div , Expr divVal , float changeInt2 ) {
171
174
exists ( Expr val |
175
+ (
176
+ val .getEnclosingFunction ( ) =
177
+ div .getEnclosingFunction ( ) .getACallToThisFunction ( ) .getEnclosingFunction ( ) or
178
+ val .getEnclosingFunction ( ) = div .getEnclosingFunction ( )
179
+ ) and
172
180
val .getValue ( ) .toFloat ( ) = changeInt2 and
173
181
compareExprWithValue ( div , divVal , val )
174
182
)
@@ -218,7 +226,7 @@ where
218
226
changeInt = 0
219
227
or
220
228
// Denominator can be sum or difference.
221
- pragma [ only_bind_into ] ( changeInt ) = getValueOperand ( div .getRV ( ) , findVal .getAnExpr ( ) , _) and
229
+ changeInt = getValueOperand ( div .getRV ( ) , findVal .getAnExpr ( ) , _) and
222
230
mayBeReturnValue ( fn , changeInt )
223
231
) and
224
232
exp = div and
@@ -246,14 +254,13 @@ where
246
254
changeInt2 = 0
247
255
or
248
256
// Denominator can be sum or difference.
249
- pragma [ only_bind_into ] ( changeInt ) =
250
- getValueOperand ( divFc .getArgument ( posArg ) , findVal .getAnExpr ( ) , _) and
257
+ changeInt = getValueOperand ( divFc .getArgument ( posArg ) , findVal .getAnExpr ( ) , _) and
251
258
mayBeReturnValue ( fn , changeInt ) and
252
259
changeInt2 = 0
253
260
)
254
261
or
255
262
// Look for a situation where the difference or subtraction is considered as an argument, and it can be used in the same way.
256
- pragma [ only_bind_into ] ( changeInt ) = getValueOperand ( div .getRV ( ) , divVal , _) and
263
+ changeInt = getValueOperand ( div .getRV ( ) , divVal , _) and
257
264
changeInt2 = changeInt and
258
265
mayBeReturnValue ( fn , changeInt ) and
259
266
divFc .getArgument ( posArg ) = findVal .getAnExpr ( )
0 commit comments