@@ -452,18 +452,22 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
452452 private predicate notExpectsContent ( NodeEx n ) { not expectsContentCached ( n .asNode ( ) , _) }
453453
454454 pragma [ nomagic]
455- private predicate hasReadStep ( Content c ) { read ( _, c , _) }
456-
457- pragma [ nomagic]
458- private predicate storeEx (
455+ private predicate storeExUnrestricted (
459456 NodeEx node1 , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
460457 ) {
461458 store ( pragma [ only_bind_into ] ( node1 .asNode ( ) ) , c , pragma [ only_bind_into ] ( node2 .asNode ( ) ) ,
462459 contentType , containerType ) and
463- hasReadStep ( c ) and
464460 stepFilter ( node1 , node2 )
465461 }
466462
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+
467471 pragma [ nomagic]
468472 private predicate viableReturnPosOutEx ( DataFlowCall call , ReturnPosition pos , NodeEx out ) {
469473 viableReturnPosOut ( call , pos , out .asNode ( ) )
@@ -5141,7 +5145,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
51415145 midNode = mid .getNodeEx ( ) and
51425146 t1 = mid .getType ( ) and
51435147 ap1 = mid .getAp ( ) and
5144- storeEx ( midNode , c , node , contentType , t2 ) and
5148+ storeExUnrestricted ( midNode , c , node , contentType , t2 ) and
51455149 ap2 .getHead ( ) = c and
51465150 ap2 .len ( ) = unbindInt ( ap1 .len ( ) + 1 ) and
51475151 compatibleTypes ( t1 , contentType )
@@ -5318,7 +5322,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
53185322 not outBarrier ( node , state ) and
53195323 // if a node is not the target of a store, we can check `clearsContent` immediately
53205324 (
5321- storeEx ( _, _, node , _, _)
5325+ storeExUnrestricted ( _, _, node , _, _)
53225326 or
53235327 not clearsContentEx ( node , ap .getHead ( ) )
53245328 )
@@ -5459,7 +5463,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
54595463 exists ( NodeEx midNode |
54605464 midNode = mid .getNodeEx ( ) and
54615465 ap = mid .getAp ( ) and
5462- storeEx ( node , c , midNode , _, _) and
5466+ storeExUnrestricted ( node , c , midNode , _, _) and
54635467 ap .getHead ( ) = c
54645468 )
54655469 }
0 commit comments