@@ -36,7 +36,7 @@ predicate boundedDiv(Expr e, Expr left) { e = left }
36
36
37
37
/**
38
38
* An operand `e` of a remainder expression `rem` (i.e., `rem` is either a `RemExpr` or
39
- * an `AssignRemExpr`) with left-hand side `left` and right-ahnd side `right` is bounded
39
+ * an `AssignRemExpr`) with left-hand side `left` and right-hand side `right` is bounded
40
40
* when `e` is `left` and `right` is upper bounded by some number that is less than the maximum integer
41
41
* allowed by the result type of `rem`.
42
42
*/
@@ -59,10 +59,17 @@ predicate boundedBitwiseAnd(Expr e, Expr andExpr, Expr operand1, Expr operand2)
59
59
}
60
60
61
61
/**
62
- * Holds if `fc ` is a part of the left operand of a binary operation that greatly reduces the range
63
- * of possible values.
62
+ * Holds if `e ` is an arithmetic expression that cannot overflow, or if `e` is an operand of an
63
+ * operation that may greatly reduces the range of possible values.
64
64
*/
65
65
predicate bounded ( Expr e ) {
66
+ (
67
+ e instanceof UnaryArithmeticOperation or
68
+ e instanceof BinaryArithmeticOperation or
69
+ e instanceof AssignArithmeticOperation
70
+ ) and
71
+ not convertedExprMightOverflow ( e )
72
+ or
66
73
// For `%` and `&` we require that `e` is bounded by a value that is strictly smaller than the
67
74
// maximum possible value of the result type of the operation.
68
75
// For example, the function call `rand()` is considered bounded in the following program:
@@ -85,7 +92,7 @@ predicate bounded(Expr e) {
85
92
boundedBitwiseAnd ( e , andExpr , andExpr .getAnOperand ( ) , andExpr .getAnOperand ( ) )
86
93
)
87
94
or
88
- // Optimitically assume that a division always yields a much smaller value.
95
+ // Optimitically assume that a division or right shift always yields a much smaller value.
89
96
boundedDiv ( e , any ( DivExpr div ) .getLeftOperand ( ) )
90
97
or
91
98
boundedDiv ( e , any ( AssignDivExpr div ) .getLValue ( ) )
0 commit comments