@@ -131,20 +131,12 @@ private class NarrowingCastExpr extends ConvertOrBoxExpr {
131
131
signature module DeltaSig {
132
132
class Delta ;
133
133
134
- bindingset [ d]
135
- bindingset [ result ]
136
134
float toFloat ( Delta d ) ;
137
135
138
- bindingset [ d]
139
- bindingset [ result ]
140
136
int toInt ( Delta d ) ;
141
137
142
- bindingset [ n]
143
- bindingset [ result ]
144
138
Delta fromInt ( int n ) ;
145
139
146
- bindingset [ f]
147
- bindingset [ result ]
148
140
Delta fromFloat ( float f ) ;
149
141
}
150
142
@@ -352,13 +344,14 @@ module RangeStage<DeltaSig D, UtilSig<D> UtilParam> {
352
344
or
353
345
// guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
354
346
// exists a guard `guardEq` such that `v = v2 - d1 + d2`.
355
- exists ( SemSsaVariable v2 , SemGuard guardEq , boolean eqIsTrue , float d1 , float d2 |
347
+ exists ( SemSsaVariable v2 , SemGuard guardEq , boolean eqIsTrue , float d1 , float d2 , float oldDelta |
356
348
guardEq =
357
349
UtilParam:: semEqFlowCond ( v , UtilParam:: semSsaRead ( v2 , D:: fromFloat ( d1 ) ) , D:: fromFloat ( d2 ) ,
358
350
true , eqIsTrue ) and
359
- result = boundFlowCond ( v2 , e , delta + d1 - d2 , upper , testIsTrue ) and
351
+ result = boundFlowCond ( v2 , e , oldDelta , upper , testIsTrue ) and
360
352
// guardEq needs to control guard
361
- guardEq .directlyControls ( result .getBasicBlock ( ) , eqIsTrue )
353
+ guardEq .directlyControls ( result .getBasicBlock ( ) , eqIsTrue ) and
354
+ delta = oldDelta - d1 + d2
362
355
)
363
356
}
364
357
0 commit comments