@@ -99,12 +99,11 @@ VariableAccess varUse(LocalScopeVariable v) { result = v.getAnAccess() }
99
99
* Holds if `e` potentially overflows and `use` is an operand of `e` that is not guarded.
100
100
*/
101
101
predicate 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
108
107
use = e .getAnOperand ( ) and
109
108
exists ( LocalScopeVariable v | use .getTarget ( ) = v |
110
109
// overflow possible if large
@@ -126,12 +125,11 @@ predicate missingGuardAgainstOverflow(Operation e, VariableAccess use) {
126
125
* Holds if `e` potentially underflows and `use` is an operand of `e` that is not guarded.
127
126
*/
128
127
predicate 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
135
133
use = e .getAnOperand ( ) and
136
134
exists ( LocalScopeVariable v | use .getTarget ( ) = v |
137
135
// underflow possible if use is left operand and small
0 commit comments