@@ -941,6 +941,17 @@ module RangeStage<
941
941
semExprDoesntOverflow ( upper .booleanNot ( ) , e )
942
942
or
943
943
not potentiallyOverflowingExpr ( upper .booleanNot ( ) , e )
944
+ or
945
+ initialBounded ( e , any ( SemZeroBound z ) , _, upper .booleanNot ( ) , _, _, _)
946
+ or
947
+ exists ( D:: Delta otherDelta |
948
+ initialBounded ( e , _, otherDelta , upper .booleanNot ( ) , _, _, _) and
949
+ (
950
+ upper = true and D:: toFloat ( otherDelta ) >= 0
951
+ or
952
+ upper = false and D:: toFloat ( otherDelta ) <= 0
953
+ )
954
+ )
944
955
)
945
956
}
946
957
@@ -952,16 +963,14 @@ module RangeStage<
952
963
(
953
964
positively = true and
954
965
(
955
- not semExprSign ( expr .( SemBinaryExpr ) .getLeftOperand ( ) ) = TPos ( )
956
- or
957
- not semExprSign ( expr .( SemBinaryExpr ) .getRightOperand ( ) ) = TPos ( )
966
+ semExprSign ( expr .( SemBinaryExpr ) .getLeftOperand ( ) ) = TPos ( ) and
967
+ semExprSign ( expr .( SemBinaryExpr ) .getRightOperand ( ) ) = TPos ( )
958
968
)
959
969
or
960
970
positively = false and
961
971
(
962
- not semExprSign ( expr .( SemBinaryExpr ) .getLeftOperand ( ) ) = TNeg ( )
963
- or
964
- not semExprSign ( expr .( SemBinaryExpr ) .getRightOperand ( ) ) = TNeg ( )
972
+ semExprSign ( expr .( SemBinaryExpr ) .getLeftOperand ( ) ) = TNeg ( ) and
973
+ semExprSign ( expr .( SemBinaryExpr ) .getRightOperand ( ) ) = TNeg ( )
965
974
)
966
975
)
967
976
or
@@ -972,16 +981,14 @@ module RangeStage<
972
981
(
973
982
positively = true and
974
983
(
975
- not semExprSign ( expr .( SemBinaryExpr ) .getLeftOperand ( ) ) = TPos ( )
976
- or
977
- not semExprSign ( expr .( SemBinaryExpr ) .getRightOperand ( ) ) = TNeg ( )
984
+ semExprSign ( expr .( SemBinaryExpr ) .getLeftOperand ( ) ) = TPos ( ) and
985
+ semExprSign ( expr .( SemBinaryExpr ) .getRightOperand ( ) ) = TNeg ( )
978
986
)
979
987
or
980
988
positively = false and
981
989
(
982
- not semExprSign ( expr .( SemBinaryExpr ) .getLeftOperand ( ) ) = TNeg ( )
983
- or
984
- not semExprSign ( expr .( SemBinaryExpr ) .getRightOperand ( ) ) = TPos ( )
990
+ semExprSign ( expr .( SemBinaryExpr ) .getLeftOperand ( ) ) = TNeg ( ) and
991
+ semExprSign ( expr .( SemBinaryExpr ) .getRightOperand ( ) ) = TPos ( )
985
992
)
986
993
)
987
994
or
0 commit comments