@@ -455,27 +455,42 @@ module MakeImplContentDataFlow<LocationSig Location, InputSig<Location> Lang> {
455
455
)
456
456
}
457
457
458
+ pragma [ nomagic]
459
+ private predicate nodeAndState ( Flow:: PathNode n , Node node , State state ) {
460
+ n .getNode ( ) = node and n .getState ( ) = state
461
+ }
462
+
463
+ pragma [ nomagic]
464
+ private predicate succNodeAndState (
465
+ Flow:: PathNode pre , Node preNode , State preState , Flow:: PathNode succ , Node succNode ,
466
+ State succState
467
+ ) {
468
+ nodeAndState ( pre , preNode , preState ) and
469
+ nodeAndState ( succ , succNode , succState ) and
470
+ pre .getASuccessor ( ) = succ
471
+ }
472
+
458
473
pragma [ nomagic]
459
474
private predicate nodeReachesStore (
460
- Flow:: PathNode source , AccessPath scReads , AccessPath scStores , Flow:: PathNode node ,
475
+ Flow:: PathNode source , AccessPath scReads , AccessPath scStores , Flow:: PathNode target ,
461
476
ContentSet c , AccessPath reads , AccessPath stores
462
477
) {
463
- exists ( Flow:: PathNode mid |
478
+ exists ( Flow:: PathNode mid , State midState , Node midNode , State targetState , Node targetNode |
464
479
nodeReaches ( source , scReads , scStores , mid , reads , stores ) and
465
- storeStep ( mid . getNode ( ) , mid . getState ( ) , c , node . getNode ( ) , node . getState ( ) ) and
466
- mid . getASuccessor ( ) = node
480
+ succNodeAndState ( mid , midNode , midState , target , targetNode , targetState ) and
481
+ storeStep ( midNode , midState , c , targetNode , targetState )
467
482
)
468
483
}
469
484
470
485
pragma [ nomagic]
471
486
private predicate nodeReachesRead (
472
- Flow:: PathNode source , AccessPath scReads , AccessPath scStores , Flow:: PathNode node ,
487
+ Flow:: PathNode source , AccessPath scReads , AccessPath scStores , Flow:: PathNode target ,
473
488
ContentSet c , AccessPath reads , AccessPath stores
474
489
) {
475
- exists ( Flow:: PathNode mid |
490
+ exists ( Flow:: PathNode mid , State midState , Node midNode , State targetState , Node targetNode |
476
491
nodeReaches ( source , scReads , scStores , mid , reads , stores ) and
477
- readStep ( mid . getNode ( ) , mid . getState ( ) , c , node . getNode ( ) , node . getState ( ) ) and
478
- mid . getASuccessor ( ) = node
492
+ succNodeAndState ( mid , midNode , midState , target , targetNode , targetState ) and
493
+ readStep ( midNode , midState , c , targetNode , targetState )
479
494
)
480
495
}
481
496
0 commit comments