@@ -62,7 +62,6 @@ predicate mayBeReturnZero(Function fn) {
6262}
6363
6464/** Gets the Guard which compares the expression `bound` */
65- pragma [ inline]
6665GuardCondition checkByValue ( Expr bound , Expr val ) {
6766 exists ( GuardCondition gc |
6867 (
@@ -122,6 +121,10 @@ predicate compareFunctionWithValue(Expr guardExp, Function compArg, Expr valArg)
122121pragma [ inline]
123122predicate checkConditions1 ( Expr div , Function fn , float changeInt ) {
124123 exists ( Expr val |
124+ (
125+ val .getEnclosingFunction ( ) = fn or
126+ val .getEnclosingFunction ( ) = div .getEnclosingFunction ( )
127+ ) and
125128 val .getValue ( ) .toFloat ( ) = changeInt and
126129 compareFunctionWithValue ( div , fn , val )
127130 )
@@ -169,6 +172,11 @@ predicate compareExprWithValue(Expr guardExp, Expr compArg, Expr valArg) {
169172pragma [ inline]
170173predicate checkConditions2 ( Expr div , Expr divVal , float changeInt2 ) {
171174 exists ( Expr val |
175+ (
176+ val .getEnclosingFunction ( ) =
177+ div .getEnclosingFunction ( ) .getACallToThisFunction ( ) .getEnclosingFunction ( ) or
178+ val .getEnclosingFunction ( ) = div .getEnclosingFunction ( )
179+ ) and
172180 val .getValue ( ) .toFloat ( ) = changeInt2 and
173181 compareExprWithValue ( div , divVal , val )
174182 )
@@ -218,7 +226,7 @@ where
218226 changeInt = 0
219227 or
220228 // 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
222230 mayBeReturnValue ( fn , changeInt )
223231 ) and
224232 exp = div and
@@ -246,14 +254,13 @@ where
246254 changeInt2 = 0
247255 or
248256 // 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
251258 mayBeReturnValue ( fn , changeInt ) and
252259 changeInt2 = 0
253260 )
254261 or
255262 // 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
257264 changeInt2 = changeInt and
258265 mayBeReturnValue ( fn , changeInt ) and
259266 divFc .getArgument ( posArg ) = findVal .getAnExpr ( )
0 commit comments