@@ -36,7 +36,7 @@ predicate boundedDiv(Expr e, Expr left) { e = left }
3636
3737/**
3838 * 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
4040 * when `e` is `left` and `right` is upper bounded by some number that is less than the maximum integer
4141 * allowed by the result type of `rem`.
4242 */
@@ -59,10 +59,17 @@ predicate boundedBitwiseAnd(Expr e, Expr andExpr, Expr operand1, Expr operand2)
5959}
6060
6161/**
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.
6464 */
6565predicate 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
6673 // For `%` and `&` we require that `e` is bounded by a value that is strictly smaller than the
6774 // maximum possible value of the result type of the operation.
6875 // For example, the function call `rand()` is considered bounded in the following program:
@@ -85,7 +92,7 @@ predicate bounded(Expr e) {
8592 boundedBitwiseAnd ( e , andExpr , andExpr .getAnOperand ( ) , andExpr .getAnOperand ( ) )
8693 )
8794 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.
8996 boundedDiv ( e , any ( DivExpr div ) .getLeftOperand ( ) )
9097 or
9198 boundedDiv ( e , any ( AssignDivExpr div ) .getLValue ( ) )
0 commit comments