@@ -407,27 +407,6 @@ deprecated predicate negative_overflow(Expr expr) {
407407 exprMightOverflowNegatively ( expr )
408408}
409409
410- /**
411- * Holds if the expression might overflow negatively. This predicate
412- * does not consider the possibility that the expression might overflow
413- * due to a conversion.
414- */
415- cached
416- predicate exprMightOverflowNegatively ( Expr expr ) {
417- getLowerBoundsImpl ( expr ) < exprMinVal ( expr )
418- }
419-
420- /**
421- * Holds if the expression might overflow negatively. Conversions
422- * are also taken into account. For example the expression
423- * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
424- * due to the addition.
425- */
426- cached
427- predicate convertedExprMightOverflowNegatively ( Expr expr ) {
428- exprMightOverflowNegatively ( expr ) or
429- convertedExprMightOverflowNegatively ( expr .getConversion ( ) )
430- }
431410
432411/**
433412 * Holds if the expression might overflow positively. This predicate
@@ -440,39 +419,6 @@ deprecated predicate positive_overflow(Expr expr) {
440419 exprMightOverflowPositively ( expr )
441420}
442421
443- /**
444- * Holds if the expression might overflow positively. This predicate
445- * does not consider the possibility that the expression might overflow
446- * due to a conversion.
447- */
448- cached
449- predicate exprMightOverflowPositively ( Expr expr ) {
450- getUpperBoundsImpl ( expr ) > exprMaxVal ( expr )
451- }
452-
453- /**
454- * Holds if the expression might overflow positively. Conversions
455- * are also taken into account. For example the expression
456- * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
457- * due to the addition.
458- */
459- cached
460- predicate convertedExprMightOverflowPositively ( Expr expr ) {
461- exprMightOverflowPositively ( expr ) or
462- convertedExprMightOverflowPositively ( expr .getConversion ( ) )
463- }
464-
465- /**
466- * Holds if the expression might overflow (either positively or
467- * negatively). The possibility that the expression might overflow
468- * due to an implicit or explicit cast is also considered.
469- */
470- cached
471- predicate convertedExprMightOverflow ( Expr expr ) {
472- convertedExprMightOverflowNegatively ( expr ) or
473- convertedExprMightOverflowPositively ( expr )
474- }
475-
476422/** Only to be called by `getTruncatedLowerBounds`. */
477423private
478424float getLowerBoundsImpl ( Expr expr ) {
@@ -1195,4 +1141,59 @@ private cached module SimpleRangeAnalysisCached {
11951141 defMightOverflowNegatively ( def , v ) or
11961142 defMightOverflowPositively ( def , v )
11971143 }
1144+
1145+ /**
1146+ * Holds if the expression might overflow negatively. This predicate
1147+ * does not consider the possibility that the expression might overflow
1148+ * due to a conversion.
1149+ */
1150+ cached
1151+ predicate exprMightOverflowNegatively ( Expr expr ) {
1152+ getLowerBoundsImpl ( expr ) < exprMinVal ( expr )
1153+ }
1154+
1155+ /**
1156+ * Holds if the expression might overflow negatively. Conversions
1157+ * are also taken into account. For example the expression
1158+ * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
1159+ * due to the addition.
1160+ */
1161+ cached
1162+ predicate convertedExprMightOverflowNegatively ( Expr expr ) {
1163+ exprMightOverflowNegatively ( expr ) or
1164+ convertedExprMightOverflowNegatively ( expr .getConversion ( ) )
1165+ }
1166+
1167+ /**
1168+ * Holds if the expression might overflow positively. This predicate
1169+ * does not consider the possibility that the expression might overflow
1170+ * due to a conversion.
1171+ */
1172+ cached
1173+ predicate exprMightOverflowPositively ( Expr expr ) {
1174+ getUpperBoundsImpl ( expr ) > exprMaxVal ( expr )
1175+ }
1176+
1177+ /**
1178+ * Holds if the expression might overflow positively. Conversions
1179+ * are also taken into account. For example the expression
1180+ * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
1181+ * due to the addition.
1182+ */
1183+ cached
1184+ predicate convertedExprMightOverflowPositively ( Expr expr ) {
1185+ exprMightOverflowPositively ( expr ) or
1186+ convertedExprMightOverflowPositively ( expr .getConversion ( ) )
1187+ }
1188+
1189+ /**
1190+ * Holds if the expression might overflow (either positively or
1191+ * negatively). The possibility that the expression might overflow
1192+ * due to an implicit or explicit cast is also considered.
1193+ */
1194+ cached
1195+ predicate convertedExprMightOverflow ( Expr expr ) {
1196+ convertedExprMightOverflowNegatively ( expr ) or
1197+ convertedExprMightOverflowPositively ( expr )
1198+ }
11981199}
0 commit comments