@@ -858,6 +858,7 @@ private module Stage1 {
858858 pragma [ nomagic]
859859 predicate revFlow ( NodeEx node , Configuration config ) { revFlow ( node , _, config ) }
860860
861+ bindingset [ node, state, config]
861862 predicate revFlow (
862863 NodeEx node , FlowState state , boolean toReturn , ApOption returnAp , Ap ap , Configuration config
863864 ) {
@@ -1110,6 +1111,8 @@ private module Stage2 {
11101111 bindingset [ node, cc, config]
11111112 private LocalCc getLocalCc ( NodeEx node , Cc cc , Configuration config ) { any ( ) }
11121113
1114+ bindingset [ node1, state1, config]
1115+ bindingset [ node2, state2, config]
11131116 private predicate localStep (
11141117 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
11151118 ApNil ap , Configuration config , LocalCc lcc
@@ -1145,6 +1148,7 @@ private module Stage2 {
11451148 private predicate typecheckStore ( Ap ap , DataFlowType contentType ) { any ( ) }
11461149
11471150 /* Begin: Stage 2 logic. */
1151+ bindingset [ node, state, config]
11481152 private predicate flowCand ( NodeEx node , FlowState state , ApApprox apa , Configuration config ) {
11491153 PrevStage:: revFlow ( node , state , _, _, apa , config )
11501154 }
@@ -1907,6 +1911,7 @@ private module Stage3 {
19071911 }
19081912
19091913 /* Begin: Stage 3 logic. */
1914+ bindingset [ node, state, config]
19101915 private predicate flowCand ( NodeEx node , FlowState state , ApApprox apa , Configuration config ) {
19111916 PrevStage:: revFlow ( node , state , _, _, apa , config )
19121917 }
@@ -2732,6 +2737,7 @@ private module Stage4 {
27322737 private predicate typecheckStore ( Ap ap , DataFlowType contentType ) { any ( ) }
27332738
27342739 /* Begin: Stage 4 logic. */
2740+ bindingset [ node, state, config]
27352741 private predicate flowCand ( NodeEx node , FlowState state , ApApprox apa , Configuration config ) {
27362742 PrevStage:: revFlow ( node , state , _, _, apa , config )
27372743 }
@@ -4452,13 +4458,22 @@ private module FlowExploration {
44524458 }
44534459 }
44544460
4461+ private predicate relevantState ( FlowState state ) {
4462+ sourceNode ( _, state , _) or
4463+ sinkNode ( _, state , _) or
4464+ additionalLocalStateStep ( _, state , _, _, _) or
4465+ additionalLocalStateStep ( _, _, _, state , _) or
4466+ additionalJumpStateStep ( _, state , _, _, _) or
4467+ additionalJumpStateStep ( _, _, _, state , _)
4468+ }
4469+
44554470 private newtype TSummaryCtx1 =
44564471 TSummaryCtx1None ( ) or
44574472 TSummaryCtx1Param ( ParamNodeEx p )
44584473
44594474 private newtype TSummaryCtx2 =
44604475 TSummaryCtx2None ( ) or
4461- TSummaryCtx2Some ( FlowState s )
4476+ TSummaryCtx2Some ( FlowState s ) { relevantState ( s ) }
44624477
44634478 private newtype TSummaryCtx3 =
44644479 TSummaryCtx3None ( ) or
@@ -4470,7 +4485,7 @@ private module FlowExploration {
44704485
44714486 private newtype TRevSummaryCtx2 =
44724487 TRevSummaryCtx2None ( ) or
4473- TRevSummaryCtx2Some ( FlowState s )
4488+ TRevSummaryCtx2Some ( FlowState s ) { relevantState ( s ) }
44744489
44754490 private newtype TRevSummaryCtx3 =
44764491 TRevSummaryCtx3None ( ) or
0 commit comments