@@ -104,8 +104,6 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
104
104
additionalStep ( node1 , state1 , node2 , state2 )
105
105
}
106
106
107
- predicate isAdditionalFlowStep = ContentConfig:: isAdditionalFlowStep / 2 ;
108
-
109
107
predicate isBarrier = ContentConfig:: isBarrier / 1 ;
110
108
111
109
FlowFeature getAFeature ( ) { result = ContentConfig:: getAFeature ( ) }
@@ -302,12 +300,16 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
302
300
// relation, when flow can reach a sink without going back out
303
301
Flow:: PathGraph:: subpaths ( pred , succ , _, _) and
304
302
not reachesSink ( succ )
305
- or
303
+ )
304
+ or
305
+ exists ( Node predNode , State predState , Node succNode , State succState |
306
+ succNodeAndState ( pred , predNode , predState , succ , succNode , succState )
307
+ |
306
308
// needed to record store steps
307
- storeStep ( pred . getNode ( ) , pred . getState ( ) , _, succ . getNode ( ) , succ . getState ( ) )
309
+ storeStep ( predNode , predState , _, succNode , succState )
308
310
or
309
311
// needed to record read steps
310
- readStep ( pred . getNode ( ) , pred . getState ( ) , _, succ . getNode ( ) , succ . getState ( ) )
312
+ readStep ( predNode , predState , _, succNode , succState )
311
313
)
312
314
}
313
315
0 commit comments