@@ -1533,11 +1533,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1533
1533
)
1534
1534
or
1535
1535
// read
1536
- exists ( Typ t0 , Ap ap0 , Content c |
1537
- fwdFlowRead ( t0 , ap0 , c , _, node , state , cc , summaryCtx ) and
1538
- fwdFlowConsCand ( t0 , ap0 , c , t , ap ) and
1539
- apa = getApprox ( ap )
1540
- )
1536
+ fwdFlowRead ( _, _, _, _, node , t , ap , state , cc , summaryCtx ) and
1537
+ apa = getApprox ( ap )
1541
1538
or
1542
1539
// flow into a callable without summary context
1543
1540
fwdFlowInNoFlowThrough ( node , apa , state , cc , t , ap ) and
@@ -1676,7 +1673,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1676
1673
}
1677
1674
1678
1675
pragma [ nomagic]
1679
- private predicate fwdFlowRead (
1676
+ private predicate fwdFlowRead0 (
1680
1677
Typ t , Ap ap , Content c , NodeEx node1 , NodeEx node2 , FlowState state , Cc cc ,
1681
1678
SummaryCtx summaryCtx
1682
1679
) {
@@ -1689,6 +1686,15 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1689
1686
)
1690
1687
}
1691
1688
1689
+ pragma [ nomagic]
1690
+ private predicate fwdFlowRead (
1691
+ NodeEx node1 , Typ t1 , Ap ap1 , Content c , NodeEx node2 , Typ t2 , Ap ap2 , FlowState state ,
1692
+ Cc cc , SummaryCtx summaryCtx
1693
+ ) {
1694
+ fwdFlowRead0 ( t1 , ap1 , c , node1 , node2 , state , cc , summaryCtx ) and
1695
+ fwdFlowConsCand ( t1 , ap1 , c , t2 , ap2 )
1696
+ }
1697
+
1692
1698
pragma [ nomagic]
1693
1699
private predicate fwdFlowIntoArg (
1694
1700
ArgNodeEx arg , FlowState state , Cc outercc , SummaryCtx summaryCtx , Typ t , Ap ap ,
@@ -2127,10 +2133,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2127
2133
2128
2134
pragma [ nomagic]
2129
2135
private predicate readStepFwd ( NodeEx n1 , Ap ap1 , Content c , NodeEx n2 , Ap ap2 ) {
2130
- exists ( Typ t1 |
2131
- fwdFlowRead ( t1 , ap1 , c , n1 , n2 , _, _, _) and
2132
- fwdFlowConsCand ( t1 , ap1 , c , _, ap2 )
2133
- )
2136
+ fwdFlowRead ( n1 , _, ap1 , c , n2 , _, ap2 , _, _, _)
2134
2137
}
2135
2138
2136
2139
pragma [ nomagic]
@@ -3200,10 +3203,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3200
3203
)
3201
3204
or
3202
3205
// read
3203
- exists ( NodeEx mid , Typ t0 , Ap ap0 , Content c |
3206
+ exists ( NodeEx mid , Typ t0 , Ap ap0 |
3204
3207
pn1 = TPathNodeMid ( mid , state , cc , summaryCtx , t0 , ap0 ) and
3205
- fwdFlowRead ( t0 , ap0 , c , mid , node , state , cc , summaryCtx ) and
3206
- fwdFlowConsCand ( t0 , ap0 , c , t , ap ) and
3208
+ fwdFlowRead ( mid , t0 , ap0 , _, node , t , ap , state , cc , summaryCtx ) and
3207
3209
label = "" and
3208
3210
isStoreStep = false
3209
3211
)
0 commit comments