66import cpp
77import semmle.code.cpp.controlflow.Dominance
88import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
9+ import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
910
1011/**
1112 * Holds if the value of `use` is guarded using `abs`.
@@ -98,7 +99,12 @@ VariableAccess varUse(LocalScopeVariable v) { result = v.getAnAccess() }
9899 * Holds if `e` potentially overflows and `use` is an operand of `e` that is not guarded.
99100 */
100101predicate missingGuardAgainstOverflow ( Operation e , VariableAccess use ) {
101- convertedExprMightOverflowPositively ( e ) and
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
102108 use = e .getAnOperand ( ) and
103109 exists ( LocalScopeVariable v | use .getTarget ( ) = v |
104110 // overflow possible if large
@@ -120,7 +126,12 @@ predicate missingGuardAgainstOverflow(Operation e, VariableAccess use) {
120126 * Holds if `e` potentially underflows and `use` is an operand of `e` that is not guarded.
121127 */
122128predicate missingGuardAgainstUnderflow ( Operation e , VariableAccess use ) {
123- convertedExprMightOverflowNegatively ( e ) and
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
124135 use = e .getAnOperand ( ) and
125136 exists ( LocalScopeVariable v | use .getTarget ( ) = v |
126137 // underflow possible if use is left operand and small
0 commit comments