@@ -104,8 +104,6 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
104104 additionalStep ( node1 , state1 , node2 , state2 )
105105 }
106106
107- predicate isAdditionalFlowStep = ContentConfig:: isAdditionalFlowStep / 2 ;
108-
109107 predicate isBarrier = ContentConfig:: isBarrier / 1 ;
110108
111109 FlowFeature getAFeature ( ) { result = ContentConfig:: getAFeature ( ) }
@@ -302,12 +300,16 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
302300 // relation, when flow can reach a sink without going back out
303301 Flow:: PathGraph:: subpaths ( pred , succ , _, _) and
304302 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+ |
306308 // needed to record store steps
307- storeStep ( pred . getNode ( ) , pred . getState ( ) , _, succ . getNode ( ) , succ . getState ( ) )
309+ storeStep ( predNode , predState , _, succNode , succState )
308310 or
309311 // needed to record read steps
310- readStep ( pred . getNode ( ) , pred . getState ( ) , _, succ . getNode ( ) , succ . getState ( ) )
312+ readStep ( predNode , predState , _, succNode , succState )
311313 )
312314 }
313315
0 commit comments