@@ -459,7 +459,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
459459 private predicate notExpectsContent ( NodeEx n ) { not expectsContentSet ( n , _) }
460460
461461 pragma [ nomagic]
462- private predicate storeExUnrestricted (
462+ private predicate storeUnrestricted (
463463 NodeEx node1 , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
464464 ) {
465465 storeEx ( node1 , c , node2 , contentType , containerType ) and
@@ -470,10 +470,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
470470 private predicate hasReadStep ( Content c ) { read ( _, c , _) }
471471
472472 pragma [ nomagic]
473- private predicate storeExRestricted (
473+ private predicate store (
474474 NodeEx node1 , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
475475 ) {
476- storeExUnrestricted ( node1 , c , node2 , contentType , containerType ) and
476+ storeUnrestricted ( node1 , c , node2 , contentType , containerType ) and
477477 hasReadStep ( c )
478478 }
479479
@@ -547,7 +547,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
547547 exists ( NodeEx mid |
548548 useFieldFlow ( ) and
549549 fwdFlow ( mid , cc ) and
550- storeExRestricted ( mid , _, node , _, _)
550+ store ( mid , _, node , _, _)
551551 )
552552 or
553553 // read
@@ -642,7 +642,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
642642 not fullBarrier ( node ) and
643643 useFieldFlow ( ) and
644644 fwdFlow ( mid , _) and
645- storeExRestricted ( mid , c , node , _, _)
645+ store ( mid , c , node , _, _)
646646 )
647647 }
648648
@@ -785,7 +785,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
785785 exists ( NodeEx mid |
786786 revFlow ( mid , toReturn ) and
787787 fwdFlowConsCand ( c ) and
788- storeExRestricted ( node , c , mid , _, _)
788+ store ( node , c , mid , _, _)
789789 )
790790 }
791791
@@ -882,7 +882,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
882882 ) {
883883 revFlowIsReadAndStored ( c ) and
884884 revFlow ( node2 ) and
885- storeExRestricted ( node1 , c , node2 , contentType , containerType ) and
885+ store ( node1 , c , node2 , contentType , containerType ) and
886886 exists ( ap1 )
887887 }
888888
@@ -5352,7 +5352,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
53525352 midNode = mid .getNodeEx ( ) and
53535353 t1 = mid .getType ( ) and
53545354 ap1 = mid .getAp ( ) and
5355- storeExUnrestricted ( midNode , c , node , contentType , t2 ) and
5355+ storeUnrestricted ( midNode , c , node , contentType , t2 ) and
53565356 ap2 .getHead ( ) = c and
53575357 ap2 .len ( ) = unbindInt ( ap1 .len ( ) + 1 ) and
53585358 compatibleTypesFilter ( t1 , contentType )
@@ -5523,7 +5523,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
55235523 not outBarrier ( node , state ) and
55245524 // if a node is not the target of a store, we can check `clearsContent` immediately
55255525 (
5526- storeExUnrestricted ( _, _, node , _, _)
5526+ storeUnrestricted ( _, _, node , _, _)
55275527 or
55285528 not clearsContentEx ( node , ap .getHead ( ) )
55295529 )
@@ -5664,7 +5664,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
56645664 exists ( NodeEx midNode |
56655665 midNode = mid .getNodeEx ( ) and
56665666 ap = mid .getAp ( ) and
5667- storeExUnrestricted ( node , c , midNode , _, _) and
5667+ storeUnrestricted ( node , c , midNode , _, _) and
56685668 ap .getHead ( ) = c
56695669 )
56705670 }
0 commit comments