@@ -455,27 +455,39 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
455455 )
456456 }
457457
458+ pragma [ nomagic]
459+ private predicate succNodeAndState (
460+ Flow:: PathNode pre , Node preNode , State preState , Flow:: PathNode succ , Node succNode ,
461+ State succState
462+ ) {
463+ pre .getNode ( ) = preNode and
464+ pre .getState ( ) = preState and
465+ succ .getNode ( ) = succNode and
466+ succ .getState ( ) = succState and
467+ pre .getASuccessor ( ) = succ
468+ }
469+
458470 pragma [ nomagic]
459471 private predicate nodeReachesStore (
460- Flow:: PathNode source , AccessPath scReads , AccessPath scStores , Flow:: PathNode node ,
472+ Flow:: PathNode source , AccessPath scReads , AccessPath scStores , Flow:: PathNode target ,
461473 ContentSet c , AccessPath reads , AccessPath stores
462474 ) {
463- exists ( Flow:: PathNode mid |
475+ exists ( Flow:: PathNode mid , State midState , Node midNode , State targetState , Node targetNode |
464476 nodeReaches ( source , scReads , scStores , mid , reads , stores ) and
465- storeStep ( mid . getNode ( ) , mid . getState ( ) , c , node . getNode ( ) , node . getState ( ) ) and
466- mid . getASuccessor ( ) = node
477+ succNodeAndState ( mid , midNode , midState , target , targetNode , targetState ) and
478+ storeStep ( midNode , midState , c , targetNode , targetState )
467479 )
468480 }
469481
470482 pragma [ nomagic]
471483 private predicate nodeReachesRead (
472- Flow:: PathNode source , AccessPath scReads , AccessPath scStores , Flow:: PathNode node ,
484+ Flow:: PathNode source , AccessPath scReads , AccessPath scStores , Flow:: PathNode target ,
473485 ContentSet c , AccessPath reads , AccessPath stores
474486 ) {
475- exists ( Flow:: PathNode mid |
487+ exists ( Flow:: PathNode mid , State midState , Node midNode , State targetState , Node targetNode |
476488 nodeReaches ( source , scReads , scStores , mid , reads , stores ) and
477- readStep ( mid . getNode ( ) , mid . getState ( ) , c , node . getNode ( ) , node . getState ( ) ) and
478- mid . getASuccessor ( ) = node
489+ succNodeAndState ( mid , midNode , midState , target , targetNode , targetState ) and
490+ readStep ( midNode , midState , c , targetNode , targetState )
479491 )
480492 }
481493
0 commit comments