@@ -99,12 +99,11 @@ VariableAccess varUse(LocalScopeVariable v) { result = v.getAnAccess() }
9999 * Holds if `e` potentially overflows and `use` is an operand of `e` that is not guarded.
100100 */
101101predicate missingGuardAgainstOverflow ( Operation e , VariableAccess use ) {
102- (
103- convertedExprMightOverflowPositively ( e )
104- or
105- // Ensure that the predicate holds when range analysis cannot determine an upper bound
106- upperBound ( e .getFullyConverted ( ) ) = exprMaxVal ( e .getFullyConverted ( ) )
107- ) and
102+ // Since `e` is guarenteed to be a `BinaryArithmeticOperation`, a `UnaryArithmeticOperation` or
103+ // an `AssignArithmeticOperation` by the other constraints in this predicate, we know that
104+ // `convertedExprMightOverflowPositively` will have a result even when `e` is not analyzable
105+ // by `SimpleRangeAnalysis`.
106+ convertedExprMightOverflowPositively ( e ) and
108107 use = e .getAnOperand ( ) and
109108 exists ( LocalScopeVariable v | use .getTarget ( ) = v |
110109 // overflow possible if large
@@ -126,12 +125,11 @@ predicate missingGuardAgainstOverflow(Operation e, VariableAccess use) {
126125 * Holds if `e` potentially underflows and `use` is an operand of `e` that is not guarded.
127126 */
128127predicate missingGuardAgainstUnderflow ( Operation e , VariableAccess use ) {
129- (
130- convertedExprMightOverflowNegatively ( e )
131- or
132- // Ensure that the predicate holds when range analysis cannot determine a lower bound
133- lowerBound ( e .getFullyConverted ( ) ) = exprMinVal ( e .getFullyConverted ( ) )
134- ) and
128+ // Since `e` is guarenteed to be a `BinaryArithmeticOperation`, a `UnaryArithmeticOperation` or
129+ // an `AssignArithmeticOperation` by the other constraints in this predicate, we know that
130+ // `convertedExprMightOverflowNegatively` will have a result even when `e` is not analyzable
131+ // by `SimpleRangeAnalysis`.
132+ convertedExprMightOverflowNegatively ( e ) and
135133 use = e .getAnOperand ( ) and
136134 exists ( LocalScopeVariable v | use .getTarget ( ) = v |
137135 // underflow possible if use is left operand and small
0 commit comments