@@ -452,18 +452,22 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
452
452
private predicate notExpectsContent ( NodeEx n ) { not expectsContentCached ( n .asNode ( ) , _) }
453
453
454
454
pragma [ nomagic]
455
- private predicate hasReadStep ( Content c ) { read ( _, c , _) }
456
-
457
- pragma [ nomagic]
458
- private predicate storeEx (
455
+ private predicate storeExUnrestricted (
459
456
NodeEx node1 , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
460
457
) {
461
458
store ( pragma [ only_bind_into ] ( node1 .asNode ( ) ) , c , pragma [ only_bind_into ] ( node2 .asNode ( ) ) ,
462
459
contentType , containerType ) and
463
- hasReadStep ( c ) and
464
460
stepFilter ( node1 , node2 )
465
461
}
466
462
463
+ pragma [ nomagic]
464
+ private predicate storeEx (
465
+ NodeEx node1 , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
466
+ ) {
467
+ storeExUnrestricted ( node1 , c , node2 , contentType , containerType ) and
468
+ read ( _, c , _)
469
+ }
470
+
467
471
pragma [ nomagic]
468
472
private predicate viableReturnPosOutEx ( DataFlowCall call , ReturnPosition pos , NodeEx out ) {
469
473
viableReturnPosOut ( call , pos , out .asNode ( ) )
@@ -5141,7 +5145,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
5141
5145
midNode = mid .getNodeEx ( ) and
5142
5146
t1 = mid .getType ( ) and
5143
5147
ap1 = mid .getAp ( ) and
5144
- storeEx ( midNode , c , node , contentType , t2 ) and
5148
+ storeExUnrestricted ( midNode , c , node , contentType , t2 ) and
5145
5149
ap2 .getHead ( ) = c and
5146
5150
ap2 .len ( ) = unbindInt ( ap1 .len ( ) + 1 ) and
5147
5151
compatibleTypes ( t1 , contentType )
@@ -5318,7 +5322,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
5318
5322
not outBarrier ( node , state ) and
5319
5323
// if a node is not the target of a store, we can check `clearsContent` immediately
5320
5324
(
5321
- storeEx ( _, _, node , _, _)
5325
+ storeExUnrestricted ( _, _, node , _, _)
5322
5326
or
5323
5327
not clearsContentEx ( node , ap .getHead ( ) )
5324
5328
)
@@ -5459,7 +5463,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
5459
5463
exists ( NodeEx midNode |
5460
5464
midNode = mid .getNodeEx ( ) and
5461
5465
ap = mid .getAp ( ) and
5462
- storeEx ( node , c , midNode , _, _) and
5466
+ storeExUnrestricted ( node , c , midNode , _, _) and
5463
5467
ap .getHead ( ) = c
5464
5468
)
5465
5469
}
0 commit comments