@@ -391,8 +391,8 @@ module Impl<FullStateConfigSig Config> {
391
391
private predicate hasReadStep ( Content c ) { read ( _, c , _) }
392
392
393
393
pragma [ nomagic]
394
- private predicate storeEx ( NodeEx node1 , TypedContent tc , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType ) {
395
- store ( pragma [ only_bind_into ] ( node1 .asNode ( ) ) , tc , c , pragma [ only_bind_into ] ( node2 .asNode ( ) ) ,
394
+ private predicate storeEx ( NodeEx node1 , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType ) {
395
+ store ( pragma [ only_bind_into ] ( node1 .asNode ( ) ) , _ , c , pragma [ only_bind_into ] ( node2 .asNode ( ) ) ,
396
396
contentType , containerType ) and
397
397
hasReadStep ( c ) and
398
398
stepFilter ( node1 , node2 )
@@ -479,7 +479,7 @@ module Impl<FullStateConfigSig Config> {
479
479
exists ( NodeEx mid |
480
480
useFieldFlow ( ) and
481
481
fwdFlow ( mid , cc ) and
482
- storeEx ( mid , _, _ , node , _, _)
482
+ storeEx ( mid , _, node , _, _)
483
483
)
484
484
or
485
485
// read
@@ -575,7 +575,7 @@ module Impl<FullStateConfigSig Config> {
575
575
not fullBarrier ( node ) and
576
576
useFieldFlow ( ) and
577
577
fwdFlow ( mid , _) and
578
- storeEx ( mid , _ , c , node , _, _)
578
+ storeEx ( mid , c , node , _, _)
579
579
)
580
580
}
581
581
@@ -712,7 +712,7 @@ module Impl<FullStateConfigSig Config> {
712
712
exists ( NodeEx mid |
713
713
revFlow ( mid , toReturn ) and
714
714
fwdFlowConsCand ( c ) and
715
- storeEx ( node , _ , c , mid , _, _)
715
+ storeEx ( node , c , mid , _, _)
716
716
)
717
717
}
718
718
@@ -802,11 +802,11 @@ module Impl<FullStateConfigSig Config> {
802
802
803
803
pragma [ nomagic]
804
804
predicate storeStepCand (
805
- NodeEx node1 , Ap ap1 , TypedContent tc , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
805
+ NodeEx node1 , Ap ap1 , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
806
806
) {
807
807
revFlowIsReadAndStored ( c ) and
808
808
revFlow ( node2 ) and
809
- storeEx ( node1 , tc , c , node2 , contentType , containerType ) and
809
+ storeEx ( node1 , c , node2 , contentType , containerType ) and
810
810
exists ( ap1 )
811
811
}
812
812
@@ -1049,7 +1049,7 @@ module Impl<FullStateConfigSig Config> {
1049
1049
predicate returnMayFlowThrough ( RetNodeEx ret , Ap argAp , Ap ap , ReturnKindExt kind ) ;
1050
1050
1051
1051
predicate storeStepCand (
1052
- NodeEx node1 , Ap ap1 , TypedContent tc , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
1052
+ NodeEx node1 , Ap ap1 , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
1053
1053
) ;
1054
1054
1055
1055
predicate readStepCand ( NodeEx n1 , Content c , NodeEx n2 ) ;
@@ -1319,7 +1319,7 @@ module Impl<FullStateConfigSig Config> {
1319
1319
) {
1320
1320
exists ( DataFlowType contentType , DataFlowType containerType , ApApprox apa1 |
1321
1321
fwdFlow ( node1 , state , cc , summaryCtx , argT , argAp , t1 , ap1 , apa1 ) and
1322
- PrevStage:: storeStepCand ( node1 , apa1 , _ , c , node2 , contentType , containerType ) and
1322
+ PrevStage:: storeStepCand ( node1 , apa1 , c , node2 , contentType , containerType ) and
1323
1323
t2 = getTyp ( containerType ) and
1324
1324
typecheckStore ( t1 , contentType )
1325
1325
)
@@ -1671,10 +1671,10 @@ module Impl<FullStateConfigSig Config> {
1671
1671
1672
1672
pragma [ nomagic]
1673
1673
predicate storeStepCand (
1674
- NodeEx node1 , Ap ap1 , TypedContent tc , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
1674
+ NodeEx node1 , Ap ap1 , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
1675
1675
) {
1676
1676
exists ( Ap ap2 |
1677
- PrevStage:: storeStepCand ( node1 , _, tc , c , node2 , contentType , containerType ) and
1677
+ PrevStage:: storeStepCand ( node1 , _, c , node2 , contentType , containerType ) and
1678
1678
revFlowStore ( ap2 , c , ap1 , _, node1 , _, node2 , _, _) and
1679
1679
revFlowConsCand ( ap2 , c , ap1 )
1680
1680
)
@@ -2023,7 +2023,7 @@ module Impl<FullStateConfigSig Config> {
2023
2023
or
2024
2024
node .asNode ( ) instanceof OutNodeExt
2025
2025
or
2026
- Stage2:: storeStepCand ( _, _, _, _ , node , _, _)
2026
+ Stage2:: storeStepCand ( _, _, _, node , _, _)
2027
2027
or
2028
2028
Stage2:: readStepCand ( _, _, node )
2029
2029
or
@@ -2046,7 +2046,7 @@ module Impl<FullStateConfigSig Config> {
2046
2046
additionalJumpStep ( node , next ) or
2047
2047
flowIntoCallNodeCand2 ( _, node , next , _) or
2048
2048
flowOutOfCallNodeCand2 ( _, node , _, next , _) or
2049
- Stage2:: storeStepCand ( node , _, _, _ , next , _, _) or
2049
+ Stage2:: storeStepCand ( node , _, _, next , _, _) or
2050
2050
Stage2:: readStepCand ( node , _, next )
2051
2051
)
2052
2052
or
@@ -3417,7 +3417,7 @@ module Impl<FullStateConfigSig Config> {
3417
3417
) {
3418
3418
t0 = mid .getType ( ) and
3419
3419
ap0 = mid .getAp ( ) and
3420
- Stage5:: storeStepCand ( mid .getNodeEx ( ) , _, _ , c , node , _, t ) and
3420
+ Stage5:: storeStepCand ( mid .getNodeEx ( ) , _, c , node , _, t ) and
3421
3421
state = mid .getState ( ) and
3422
3422
cc = mid .getCallContext ( )
3423
3423
}
@@ -3624,7 +3624,7 @@ module Impl<FullStateConfigSig Config> {
3624
3624
result .isHidden ( ) and
3625
3625
exists ( NodeEx n1 , NodeEx n2 | n1 = n .getNodeEx ( ) and n2 = result .getNodeEx ( ) |
3626
3626
localFlowBigStep ( n1 , _, n2 , _, _, _, _) or
3627
- storeEx ( n1 , _, _ , n2 , _, _) or
3627
+ storeEx ( n1 , _, n2 , _, _) or
3628
3628
readSetEx ( n1 , _, n2 )
3629
3629
)
3630
3630
}
@@ -4283,7 +4283,7 @@ module Impl<FullStateConfigSig Config> {
4283
4283
midNode = mid .getNodeEx ( ) and
4284
4284
t1 = mid .getType ( ) and
4285
4285
ap1 = mid .getAp ( ) and
4286
- storeEx ( midNode , _ , c , node , contentType , t2 ) and
4286
+ storeEx ( midNode , c , node , contentType , t2 ) and
4287
4287
ap2 .getHead ( ) = c and
4288
4288
ap2 .len ( ) = unbindInt ( ap1 .len ( ) + 1 ) and
4289
4289
compatibleTypes ( t1 , contentType )
@@ -4543,7 +4543,7 @@ module Impl<FullStateConfigSig Config> {
4543
4543
exists ( NodeEx midNode |
4544
4544
midNode = mid .getNodeEx ( ) and
4545
4545
ap = mid .getAp ( ) and
4546
- storeEx ( node , _ , c , midNode , _, _) and
4546
+ storeEx ( node , c , midNode , _, _) and
4547
4547
ap .getHead ( ) = c
4548
4548
)
4549
4549
}
0 commit comments