@@ -80,7 +80,10 @@ predicate defMightOverflowPositively(RangeSsaDefinition def, StackVariable v) {
80
80
* Holds if the definition might overflow (either positively or
81
81
* negatively).
82
82
*/
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
+ }
84
87
85
88
/**
86
89
* Holds if the expression might overflow negatively. This predicate
@@ -95,7 +98,10 @@ predicate exprMightOverflowNegatively(Expr expr) { none() }
95
98
* `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
96
99
* due to the addition.
97
100
*/
98
- predicate convertedExprMightOverflowNegatively ( Expr expr ) { none ( ) }
101
+ predicate convertedExprMightOverflowNegatively ( Expr expr ) {
102
+ exprMightOverflowNegatively ( expr ) or
103
+ convertedExprMightOverflowNegatively ( expr .getConversion ( ) )
104
+ }
99
105
100
106
/**
101
107
* Holds if the expression might overflow positively. This predicate
@@ -110,11 +116,17 @@ predicate exprMightOverflowPositively(Expr expr) { none() }
110
116
* `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
111
117
* due to the addition.
112
118
*/
113
- predicate convertedExprMightOverflowPositively ( Expr expr ) { none ( ) }
119
+ predicate convertedExprMightOverflowPositively ( Expr expr ) {
120
+ exprMightOverflowPositively ( expr ) or
121
+ convertedExprMightOverflowPositively ( expr .getConversion ( ) )
122
+ }
114
123
115
124
/**
116
125
* Holds if the expression might overflow (either positively or
117
126
* negatively). The possibility that the expression might overflow
118
127
* due to an implicit or explicit cast is also considered.
119
128
*/
120
- predicate convertedExprMightOverflow ( Expr expr ) { none ( ) }
129
+ predicate convertedExprMightOverflow ( Expr expr ) {
130
+ convertedExprMightOverflowNegatively ( expr ) or
131
+ convertedExprMightOverflowPositively ( expr )
132
+ }
0 commit comments