@@ -155,7 +155,7 @@ signature module LangSig<DeltaSig D> {
155155 /**
156156 * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
157157 */
158- predicate hasConstantBound ( SemExpr e , D:: Delta bound , boolean upper ) ;
158+ predicate hasConstantBound ( SemExpr e , D:: Delta bound , boolean upper , SemReason reason ) ;
159159
160160 /**
161161 * Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`).
@@ -920,14 +920,15 @@ module RangeStage<
920920 * Holds if `e` has an upper (for `upper = true`) or lower
921921 * (for `upper = false`) bound of `b`.
922922 */
923- private predicate baseBound ( SemExpr e , D:: Delta b , boolean upper ) {
924- hasConstantBound ( e , b , upper )
923+ private predicate baseBound ( SemExpr e , D:: Delta b , boolean upper , SemReason reason ) {
924+ hasConstantBound ( e , b , upper , reason )
925925 or
926926 upper = false and
927927 b = D:: fromInt ( 0 ) and
928928 semPositive ( e .( SemBitAndExpr ) .getAnOperand ( ) ) and
929929 // REVIEW: We let the language opt out here to preserve original results.
930- not ignoreZeroLowerBound ( e )
930+ not ignoreZeroLowerBound ( e ) and
931+ reason instanceof SemNoReason
931932 }
932933
933934 /**
@@ -1055,11 +1056,10 @@ module RangeStage<
10551056 origdelta = delta and
10561057 reason instanceof SemNoReason
10571058 or
1058- baseBound ( e , delta , upper ) and
1059+ baseBound ( e , delta , upper , reason ) and
10591060 b instanceof SemZeroBound and
10601061 fromBackEdge = false and
1061- origdelta = delta and
1062- reason instanceof SemNoReason
1062+ origdelta = delta
10631063 or
10641064 exists ( SemSsaVariable v , SemSsaReadPositionBlock bb |
10651065 boundedSsa ( v , bb , b , delta , upper , fromBackEdge , origdelta , reason ) and
0 commit comments