@@ -95,7 +95,15 @@ predicate defMightOverflow(RangeSsaDefinition def, StackVariable v) {
95
95
* does not consider the possibility that the expression might overflow
96
96
* due to a conversion.
97
97
*/
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
+ }
99
107
100
108
/**
101
109
* Holds if the expression might overflow negatively. Conversions
@@ -113,7 +121,15 @@ predicate convertedExprMightOverflowNegatively(Expr expr) {
113
121
* does not consider the possibility that the expression might overflow
114
122
* due to a conversion.
115
123
*/
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
+ }
117
133
118
134
/**
119
135
* Holds if the expression might overflow positively. Conversions
0 commit comments