@@ -455,27 +455,39 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
455
455
)
456
456
}
457
457
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
+
458
470
pragma [ nomagic]
459
471
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 ,
461
473
ContentSet c , AccessPath reads , AccessPath stores
462
474
) {
463
- exists ( Flow:: PathNode mid |
475
+ exists ( Flow:: PathNode mid , State midState , Node midNode , State targetState , Node targetNode |
464
476
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 )
467
479
)
468
480
}
469
481
470
482
pragma [ nomagic]
471
483
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 ,
473
485
ContentSet c , AccessPath reads , AccessPath stores
474
486
) {
475
- exists ( Flow:: PathNode mid |
487
+ exists ( Flow:: PathNode mid , State midState , Node midNode , State targetState , Node targetNode |
476
488
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 )
479
491
)
480
492
}
481
493
0 commit comments