@@ -838,13 +838,13 @@ private module Stage1 implements StageSig {
838
838
* by `revFlow`.
839
839
*/
840
840
pragma [ nomagic]
841
- predicate revFlowIsReadAndStored ( Content c , Configuration conf ) {
841
+ additional predicate revFlowIsReadAndStored ( Content c , Configuration conf ) {
842
842
revFlowConsCand ( c , conf ) and
843
843
revFlowStore ( c , _, _, conf )
844
844
}
845
845
846
846
pragma [ nomagic]
847
- predicate viableReturnPosOutNodeCandFwd1 (
847
+ additional predicate viableReturnPosOutNodeCandFwd1 (
848
848
DataFlowCall call , ReturnPosition pos , NodeEx out , Configuration config
849
849
) {
850
850
fwdFlowReturnPosition ( pos , _, config ) and
@@ -860,7 +860,7 @@ private module Stage1 implements StageSig {
860
860
}
861
861
862
862
pragma [ nomagic]
863
- predicate viableParamArgNodeCandFwd1 (
863
+ additional predicate viableParamArgNodeCandFwd1 (
864
864
DataFlowCall call , ParamNodeEx p , ArgNodeEx arg , Configuration config
865
865
) {
866
866
viableParamArgEx ( call , p , arg ) and
@@ -907,7 +907,7 @@ private module Stage1 implements StageSig {
907
907
)
908
908
}
909
909
910
- predicate revFlowState ( FlowState state , Configuration config ) {
910
+ additional predicate revFlowState ( FlowState state , Configuration config ) {
911
911
exists ( NodeEx node |
912
912
sinkNode ( node , state , config ) and
913
913
revFlow ( node , _, pragma [ only_bind_into ] ( config ) ) and
@@ -999,7 +999,7 @@ private module Stage1 implements StageSig {
999
999
)
1000
1000
}
1001
1001
1002
- predicate stats (
1002
+ additional predicate stats (
1003
1003
boolean fwd , int nodes , int fields , int conscand , int states , int tuples , Configuration config
1004
1004
) {
1005
1005
fwd = true and
@@ -1260,7 +1260,7 @@ private module MkStage<StageSig PrevStage> {
1260
1260
* argument.
1261
1261
*/
1262
1262
pragma [ nomagic]
1263
- predicate fwdFlow (
1263
+ additional predicate fwdFlow (
1264
1264
NodeEx node , FlowState state , Cc cc , ApOption argAp , Ap ap , Configuration config
1265
1265
) {
1266
1266
fwdFlow0 ( node , state , cc , argAp , ap , config ) and
@@ -1484,7 +1484,7 @@ private module MkStage<StageSig PrevStage> {
1484
1484
* the access path of the returned value.
1485
1485
*/
1486
1486
pragma [ nomagic]
1487
- predicate revFlow (
1487
+ additional predicate revFlow (
1488
1488
NodeEx node , FlowState state , boolean toReturn , ApOption returnAp , Ap ap , Configuration config
1489
1489
) {
1490
1490
revFlow0 ( node , state , toReturn , returnAp , ap , config ) and
@@ -1662,7 +1662,7 @@ private module MkStage<StageSig PrevStage> {
1662
1662
)
1663
1663
}
1664
1664
1665
- predicate revFlow ( NodeEx node , FlowState state , Configuration config ) {
1665
+ additional predicate revFlow ( NodeEx node , FlowState state , Configuration config ) {
1666
1666
revFlow ( node , state , _, _, _, config )
1667
1667
}
1668
1668
@@ -1675,11 +1675,13 @@ private module MkStage<StageSig PrevStage> {
1675
1675
1676
1676
// use an alias as a workaround for bad functionality-induced joins
1677
1677
pragma [ nomagic]
1678
- predicate revFlowAlias ( NodeEx node , Configuration config ) { revFlow ( node , _, _, _, _, config ) }
1678
+ additional predicate revFlowAlias ( NodeEx node , Configuration config ) {
1679
+ revFlow ( node , _, _, _, _, config )
1680
+ }
1679
1681
1680
1682
// use an alias as a workaround for bad functionality-induced joins
1681
1683
pragma [ nomagic]
1682
- predicate revFlowAlias ( NodeEx node , FlowState state , Ap ap , Configuration config ) {
1684
+ additional predicate revFlowAlias ( NodeEx node , FlowState state , Ap ap , Configuration config ) {
1683
1685
revFlow ( node , state , ap , config )
1684
1686
}
1685
1687
@@ -1700,7 +1702,7 @@ private module MkStage<StageSig PrevStage> {
1700
1702
)
1701
1703
}
1702
1704
1703
- predicate consCand ( TypedContent tc , Ap ap , Configuration config ) {
1705
+ additional predicate consCand ( TypedContent tc , Ap ap , Configuration config ) {
1704
1706
revConsCand ( tc , ap , config ) and
1705
1707
validAp ( ap , config )
1706
1708
}
@@ -1742,7 +1744,7 @@ private module MkStage<StageSig PrevStage> {
1742
1744
)
1743
1745
}
1744
1746
1745
- predicate stats (
1747
+ additional predicate stats (
1746
1748
boolean fwd , int nodes , int fields , int conscand , int states , int tuples , Configuration config
1747
1749
) {
1748
1750
fwd = true and
0 commit comments