@@ -95,7 +95,15 @@ predicate defMightOverflow(RangeSsaDefinition def, StackVariable v) {
9595 * does not consider the possibility that the expression might overflow
9696 * due to a conversion.
9797 */
98- predicate exprMightOverflowNegatively ( Expr expr ) { lowerBound ( expr ) < exprMinVal ( expr ) }
98+ predicate exprMightOverflowNegatively ( Expr expr ) {
99+ lowerBound ( expr ) < exprMinVal ( expr )
100+ or
101+ exists ( SemanticExprConfig:: Expr semExpr |
102+ semExpr .getUnconverted ( ) .getAst ( ) = expr and
103+ ConstantStage:: potentiallyOverflowingExpr ( false , semExpr ) and
104+ not ConstantStage:: initialBounded ( semExpr , _, _, false , _, _, _)
105+ )
106+ }
99107
100108/**
101109 * Holds if the expression might overflow negatively. Conversions
@@ -113,7 +121,15 @@ predicate convertedExprMightOverflowNegatively(Expr expr) {
113121 * does not consider the possibility that the expression might overflow
114122 * due to a conversion.
115123 */
116- predicate exprMightOverflowPositively ( Expr expr ) { upperBound ( expr ) > exprMaxVal ( expr ) }
124+ predicate exprMightOverflowPositively ( Expr expr ) {
125+ upperBound ( expr ) > exprMaxVal ( expr )
126+ or
127+ exists ( SemanticExprConfig:: Expr semExpr |
128+ semExpr .getUnconverted ( ) .getAst ( ) = expr and
129+ ConstantStage:: potentiallyOverflowingExpr ( true , semExpr ) and
130+ not ConstantStage:: initialBounded ( semExpr , _, _, true , _, _, _)
131+ )
132+ }
117133
118134/**
119135 * Holds if the expression might overflow positively. Conversions
0 commit comments