@@ -1204,14 +1204,6 @@ module Impl<FullStateConfigSig Config> {
1204
1204
filter ( node , state , t , ap )
1205
1205
}
1206
1206
1207
- pragma [ inline]
1208
- additional predicate fwdFlow (
1209
- NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
1210
- ApOption argAp , Typ t , Ap ap
1211
- ) {
1212
- fwdFlow ( node , state , cc , summaryCtx , argT , argAp , t , ap , _)
1213
- }
1214
-
1215
1207
pragma [ assume_small_delta]
1216
1208
pragma [ nomagic]
1217
1209
private predicate fwdFlow0 (
@@ -1359,7 +1351,7 @@ module Impl<FullStateConfigSig Config> {
1359
1351
ParamNodeOption summaryCtx , TypOption argT , ApOption argAp
1360
1352
) {
1361
1353
exists ( ApHeadContent apc |
1362
- fwdFlow ( node1 , state , cc , summaryCtx , argT , argAp , t , ap ) and
1354
+ fwdFlow ( node1 , state , cc , summaryCtx , argT , argAp , t , ap , _ ) and
1363
1355
apc = getHeadContent ( ap ) and
1364
1356
readStepCand0 ( node1 , apc , c , node2 )
1365
1357
)
@@ -1520,14 +1512,14 @@ module Impl<FullStateConfigSig Config> {
1520
1512
NodeEx node , FlowState state , ReturnCtx returnCtx , ApOption returnAp , Ap ap
1521
1513
) {
1522
1514
revFlow0 ( node , state , returnCtx , returnAp , ap ) and
1523
- fwdFlow ( node , state , _, _, _, _, _, ap )
1515
+ fwdFlow ( node , state , _, _, _, _, _, ap , _ )
1524
1516
}
1525
1517
1526
1518
pragma [ nomagic]
1527
1519
private predicate revFlow0 (
1528
1520
NodeEx node , FlowState state , ReturnCtx returnCtx , ApOption returnAp , Ap ap
1529
1521
) {
1530
- fwdFlow ( node , state , _, _, _, _, _, ap ) and
1522
+ fwdFlow ( node , state , _, _, _, _, _, ap , _ ) and
1531
1523
sinkNode ( node , state ) and
1532
1524
(
1533
1525
if hasSinkCallCtx ( )
@@ -1780,13 +1772,13 @@ module Impl<FullStateConfigSig Config> {
1780
1772
boolean fwd , int nodes , int fields , int conscand , int states , int tuples
1781
1773
) {
1782
1774
fwd = true and
1783
- nodes = count ( NodeEx node | fwdFlow ( node , _, _, _, _, _, _, _) ) and
1775
+ nodes = count ( NodeEx node | fwdFlow ( node , _, _, _, _, _, _, _, _ ) ) and
1784
1776
fields = count ( Content f0 | fwdConsCand ( f0 , _, _) ) and
1785
1777
conscand = count ( Content f0 , Typ t , Ap ap | fwdConsCand ( f0 , t , ap ) ) and
1786
- states = count ( FlowState state | fwdFlow ( _, state , _, _, _, _, _, _) ) and
1778
+ states = count ( FlowState state | fwdFlow ( _, state , _, _, _, _, _, _, _ ) ) and
1787
1779
tuples =
1788
1780
count ( NodeEx n , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
1789
- ApOption argAp , Typ t , Ap ap | fwdFlow ( n , state , cc , summaryCtx , argT , argAp , t , ap ) )
1781
+ ApOption argAp , Typ t , Ap ap | fwdFlow ( n , state , cc , summaryCtx , argT , argAp , t , ap , _ ) )
1790
1782
or
1791
1783
fwd = false and
1792
1784
nodes = count ( NodeEx node | revFlow ( node , _, _, _, _) ) and
@@ -2197,8 +2189,8 @@ module Impl<FullStateConfigSig Config> {
2197
2189
import BooleanCallContext
2198
2190
2199
2191
predicate localStep (
2200
- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2201
- DataFlowType t , LocalCc lcc
2192
+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue , Typ t ,
2193
+ LocalCc lcc
2202
2194
) {
2203
2195
localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , _) and
2204
2196
exists ( lcc )
@@ -2274,8 +2266,8 @@ module Impl<FullStateConfigSig Config> {
2274
2266
2275
2267
pragma [ nomagic]
2276
2268
predicate localStep (
2277
- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2278
- DataFlowType t , LocalCc lcc
2269
+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue , Typ t ,
2270
+ LocalCc lcc
2279
2271
) {
2280
2272
localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , _) and
2281
2273
PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
@@ -2365,7 +2357,7 @@ module Impl<FullStateConfigSig Config> {
2365
2357
exists ( AccessPathFront apf |
2366
2358
Stage4:: revFlow ( node , state , TReturnCtxMaybeFlowThrough ( _) , _, apf ) and
2367
2359
Stage4:: fwdFlow ( node , state , any ( Stage4:: CcCall ccc ) , _, _, TAccessPathFrontSome ( argApf ) , _,
2368
- apf )
2360
+ apf , _ )
2369
2361
)
2370
2362
}
2371
2363
@@ -2579,8 +2571,8 @@ module Impl<FullStateConfigSig Config> {
2579
2571
import LocalCallContext
2580
2572
2581
2573
predicate localStep (
2582
- NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2583
- DataFlowType t , LocalCc lcc
2574
+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue , Typ t ,
2575
+ LocalCc lcc
2584
2576
) {
2585
2577
localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc ) and
2586
2578
PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
@@ -2632,7 +2624,7 @@ module Impl<FullStateConfigSig Config> {
2632
2624
Stage5:: parameterMayFlowThrough ( p , _) and
2633
2625
Stage5:: revFlow ( n , state , TReturnCtxMaybeFlowThrough ( _) , _, apa0 ) and
2634
2626
Stage5:: fwdFlow ( n , state , any ( CallContextCall ccc ) , TParamNodeSome ( p .asNode ( ) ) , _,
2635
- TAccessPathApproxSome ( apa ) , _, apa0 )
2627
+ TAccessPathApproxSome ( apa ) , _, apa0 , _ )
2636
2628
)
2637
2629
}
2638
2630
@@ -2649,7 +2641,7 @@ module Impl<FullStateConfigSig Config> {
2649
2641
TSummaryCtxSome ( ParamNodeEx p , FlowState state , DataFlowType t , AccessPath ap ) {
2650
2642
exists ( AccessPathApprox apa | ap .getApprox ( ) = apa |
2651
2643
Stage5:: parameterMayFlowThrough ( p , apa ) and
2652
- Stage5:: fwdFlow ( p , state , _, _, _, _, t , apa ) and
2644
+ Stage5:: fwdFlow ( p , state , _, _, _, _, t , apa , _ ) and
2653
2645
Stage5:: revFlow ( p , state , _)
2654
2646
)
2655
2647
}
0 commit comments