@@ -459,7 +459,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
459
459
private predicate notExpectsContent ( NodeEx n ) { not expectsContentSet ( n , _) }
460
460
461
461
pragma [ nomagic]
462
- private predicate storeExUnrestricted (
462
+ private predicate storeUnrestricted (
463
463
NodeEx node1 , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
464
464
) {
465
465
storeEx ( node1 , c , node2 , contentType , containerType ) and
@@ -470,10 +470,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
470
470
private predicate hasReadStep ( Content c ) { read ( _, c , _) }
471
471
472
472
pragma [ nomagic]
473
- private predicate storeExRestricted (
473
+ private predicate store (
474
474
NodeEx node1 , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
475
475
) {
476
- storeExUnrestricted ( node1 , c , node2 , contentType , containerType ) and
476
+ storeUnrestricted ( node1 , c , node2 , contentType , containerType ) and
477
477
hasReadStep ( c )
478
478
}
479
479
@@ -547,7 +547,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
547
547
exists ( NodeEx mid |
548
548
useFieldFlow ( ) and
549
549
fwdFlow ( mid , cc ) and
550
- storeExRestricted ( mid , _, node , _, _)
550
+ store ( mid , _, node , _, _)
551
551
)
552
552
or
553
553
// read
@@ -642,7 +642,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
642
642
not fullBarrier ( node ) and
643
643
useFieldFlow ( ) and
644
644
fwdFlow ( mid , _) and
645
- storeExRestricted ( mid , c , node , _, _)
645
+ store ( mid , c , node , _, _)
646
646
)
647
647
}
648
648
@@ -785,7 +785,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
785
785
exists ( NodeEx mid |
786
786
revFlow ( mid , toReturn ) and
787
787
fwdFlowConsCand ( c ) and
788
- storeExRestricted ( node , c , mid , _, _)
788
+ store ( node , c , mid , _, _)
789
789
)
790
790
}
791
791
@@ -882,7 +882,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
882
882
) {
883
883
revFlowIsReadAndStored ( c ) and
884
884
revFlow ( node2 ) and
885
- storeExRestricted ( node1 , c , node2 , contentType , containerType ) and
885
+ store ( node1 , c , node2 , contentType , containerType ) and
886
886
exists ( ap1 )
887
887
}
888
888
@@ -5352,7 +5352,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
5352
5352
midNode = mid .getNodeEx ( ) and
5353
5353
t1 = mid .getType ( ) and
5354
5354
ap1 = mid .getAp ( ) and
5355
- storeExUnrestricted ( midNode , c , node , contentType , t2 ) and
5355
+ storeUnrestricted ( midNode , c , node , contentType , t2 ) and
5356
5356
ap2 .getHead ( ) = c and
5357
5357
ap2 .len ( ) = unbindInt ( ap1 .len ( ) + 1 ) and
5358
5358
compatibleTypesFilter ( t1 , contentType )
@@ -5523,7 +5523,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
5523
5523
not outBarrier ( node , state ) and
5524
5524
// if a node is not the target of a store, we can check `clearsContent` immediately
5525
5525
(
5526
- storeExUnrestricted ( _, _, node , _, _)
5526
+ storeUnrestricted ( _, _, node , _, _)
5527
5527
or
5528
5528
not clearsContentEx ( node , ap .getHead ( ) )
5529
5529
)
@@ -5664,7 +5664,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
5664
5664
exists ( NodeEx midNode |
5665
5665
midNode = mid .getNodeEx ( ) and
5666
5666
ap = mid .getAp ( ) and
5667
- storeExUnrestricted ( node , c , midNode , _, _) and
5667
+ storeUnrestricted ( node , c , midNode , _, _) and
5668
5668
ap .getHead ( ) = c
5669
5669
)
5670
5670
}
0 commit comments