@@ -326,7 +326,7 @@ private module Stage1 {
326326 // read
327327 exists ( Content c |
328328 fwdFlowRead ( c , node , cc , config ) and
329- fwdFlowIsStored ( c , config ) and
329+ fwdFlowConsCand ( c , config ) and
330330 not inBarrier ( node , config )
331331 )
332332 or
@@ -362,7 +362,7 @@ private module Stage1 {
362362 * Holds if `c` is the target of a store in the flow covered by `fwdFlow`.
363363 */
364364 pragma [ nomagic]
365- private predicate fwdFlowIsStored ( Content c , Configuration config ) {
365+ private predicate fwdFlowConsCand ( Content c , Configuration config ) {
366366 exists ( Node mid , Node node , TypedContent tc |
367367 not fullBarrier ( node , config ) and
368368 useFieldFlow ( config ) and
@@ -413,12 +413,12 @@ private module Stage1 {
413413 */
414414 pragma [ nomagic]
415415 predicate revFlow ( Node node , boolean toReturn , Configuration config ) {
416- revFlow_0 ( node , toReturn , config ) and
416+ revFlow0 ( node , toReturn , config ) and
417417 fwdFlow ( node , config )
418418 }
419419
420420 pragma [ nomagic]
421- private predicate revFlow_0 ( Node node , boolean toReturn , Configuration config ) {
421+ private predicate revFlow0 ( Node node , boolean toReturn , Configuration config ) {
422422 fwdFlow ( node , config ) and
423423 config .isSink ( node ) and
424424 toReturn = false
@@ -448,13 +448,13 @@ private module Stage1 {
448448 // store
449449 exists ( Content c |
450450 revFlowStore ( c , node , toReturn , config ) and
451- revFlowIsRead ( c , config )
451+ revFlowConsCand ( c , config )
452452 )
453453 or
454454 // read
455455 exists ( Node mid , Content c |
456456 read ( node , c , mid ) and
457- fwdFlowIsStored ( c , unbind ( config ) ) and
457+ fwdFlowConsCand ( c , unbind ( config ) ) and
458458 revFlow ( mid , toReturn , config )
459459 )
460460 or
@@ -479,11 +479,11 @@ private module Stage1 {
479479 * Holds if `c` is the target of a read in the flow covered by `revFlow`.
480480 */
481481 pragma [ nomagic]
482- private predicate revFlowIsRead ( Content c , Configuration config ) {
482+ private predicate revFlowConsCand ( Content c , Configuration config ) {
483483 exists ( Node mid , Node node |
484484 fwdFlow ( node , unbind ( config ) ) and
485485 read ( node , c , mid ) and
486- fwdFlowIsStored ( c , unbind ( config ) ) and
486+ fwdFlowConsCand ( c , unbind ( config ) ) and
487487 revFlow ( mid , _, config )
488488 )
489489 }
@@ -492,7 +492,7 @@ private module Stage1 {
492492 private predicate revFlowStore ( Content c , Node node , boolean toReturn , Configuration config ) {
493493 exists ( Node mid , TypedContent tc |
494494 revFlow ( mid , toReturn , config ) and
495- fwdFlowIsStored ( c , unbind ( config ) ) and
495+ fwdFlowConsCand ( c , unbind ( config ) ) and
496496 store ( node , tc , mid , _) and
497497 c = tc .getContent ( )
498498 )
@@ -503,7 +503,7 @@ private module Stage1 {
503503 * by `revFlow`.
504504 */
505505 private predicate revFlowIsReadAndStored ( Content c , Configuration conf ) {
506- revFlowIsRead ( c , conf ) and
506+ revFlowConsCand ( c , conf ) and
507507 revFlowStore ( c , _, _, conf )
508508 }
509509
@@ -587,13 +587,13 @@ private module Stage1 {
587587 predicate stats ( boolean fwd , int nodes , int fields , int conscand , int tuples , Configuration config ) {
588588 fwd = true and
589589 nodes = count ( Node node | fwdFlow ( node , config ) ) and
590- fields = count ( Content f0 | fwdFlowIsStored ( f0 , config ) ) and
590+ fields = count ( Content f0 | fwdFlowConsCand ( f0 , config ) ) and
591591 conscand = - 1 and
592592 tuples = count ( Node n , boolean b | fwdFlow ( n , b , config ) )
593593 or
594594 fwd = false and
595595 nodes = count ( Node node | revFlow ( node , _, config ) ) and
596- fields = count ( Content f0 | revFlowIsRead ( f0 , config ) ) and
596+ fields = count ( Content f0 | revFlowConsCand ( f0 , config ) ) and
597597 conscand = - 1 and
598598 tuples = count ( Node n , boolean b | revFlow ( n , b , config ) )
599599 }
0 commit comments