@@ -80,7 +80,10 @@ predicate defMightOverflowPositively(RangeSsaDefinition def, StackVariable v) {
8080 * Holds if the definition might overflow (either positively or
8181 * negatively).
8282 */
83- predicate defMightOverflow ( RangeSsaDefinition def , StackVariable v ) { none ( ) }
83+ predicate defMightOverflow ( RangeSsaDefinition def , StackVariable v ) {
84+ defMightOverflowNegatively ( def , v ) or
85+ defMightOverflowPositively ( def , v )
86+ }
8487
8588/**
8689 * Holds if the expression might overflow negatively. This predicate
@@ -95,7 +98,10 @@ predicate exprMightOverflowNegatively(Expr expr) { none() }
9598 * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
9699 * due to the addition.
97100 */
98- predicate convertedExprMightOverflowNegatively ( Expr expr ) { none ( ) }
101+ predicate convertedExprMightOverflowNegatively ( Expr expr ) {
102+ exprMightOverflowNegatively ( expr ) or
103+ convertedExprMightOverflowNegatively ( expr .getConversion ( ) )
104+ }
99105
100106/**
101107 * Holds if the expression might overflow positively. This predicate
@@ -110,11 +116,17 @@ predicate exprMightOverflowPositively(Expr expr) { none() }
110116 * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
111117 * due to the addition.
112118 */
113- predicate convertedExprMightOverflowPositively ( Expr expr ) { none ( ) }
119+ predicate convertedExprMightOverflowPositively ( Expr expr ) {
120+ exprMightOverflowPositively ( expr ) or
121+ convertedExprMightOverflowPositively ( expr .getConversion ( ) )
122+ }
114123
115124/**
116125 * Holds if the expression might overflow (either positively or
117126 * negatively). The possibility that the expression might overflow
118127 * due to an implicit or explicit cast is also considered.
119128 */
120- predicate convertedExprMightOverflow ( Expr expr ) { none ( ) }
129+ predicate convertedExprMightOverflow ( Expr expr ) {
130+ convertedExprMightOverflowNegatively ( expr ) or
131+ convertedExprMightOverflowPositively ( expr )
132+ }
0 commit comments