@@ -3740,13 +3740,14 @@ private module Subpaths {
3740
3740
*/
3741
3741
pragma [ nomagic]
3742
3742
private predicate subpaths01 (
3743
- PathNode arg , ParamNodeEx par , SummaryCtxSome sc , CallContext innercc , ReturnKindExt kind ,
3743
+ PathNodeImpl arg , ParamNodeEx par , SummaryCtxSome sc , CallContext innercc , ReturnKindExt kind ,
3744
3744
NodeEx out , AccessPath apout
3745
3745
) {
3746
3746
exists ( Configuration config |
3747
3747
pathThroughCallable ( arg , out , _, pragma [ only_bind_into ] ( apout ) ) and
3748
3748
pathIntoCallable ( arg , par , _, innercc , sc , _, config ) and
3749
- paramFlowsThrough ( kind , innercc , sc , pragma [ only_bind_into ] ( apout ) , _, unbindConf ( config ) )
3749
+ paramFlowsThrough ( kind , innercc , sc , pragma [ only_bind_into ] ( apout ) , _, unbindConf ( config ) ) and
3750
+ not arg .isHidden ( )
3750
3751
)
3751
3752
}
3752
3753
@@ -3780,21 +3781,27 @@ private module Subpaths {
3780
3781
innercc = ret .getCallContext ( ) and
3781
3782
sc = ret .getSummaryCtx ( ) and
3782
3783
ret .getConfiguration ( ) = unbindConf ( getPathNodeConf ( arg ) ) and
3783
- apout = ret .getAp ( ) and
3784
- not ret .isHidden ( )
3784
+ apout = ret .getAp ( )
3785
3785
)
3786
3786
}
3787
3787
3788
+ private PathNodeImpl localStepToHidden ( PathNodeImpl n ) {
3789
+ n .getASuccessorImpl ( ) = result and
3790
+ result .isHidden ( ) and
3791
+ localFlowBigStep ( n .getNodeEx ( ) , result .getNodeEx ( ) , _, _, _, _)
3792
+ }
3793
+
3788
3794
/**
3789
3795
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
3790
3796
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
3791
3797
* `ret -> out` is summarized as the edge `arg -> out`.
3792
3798
*/
3793
- predicate subpaths ( PathNode arg , PathNodeImpl par , PathNodeMid ret , PathNodeMid out ) {
3799
+ predicate subpaths ( PathNode arg , PathNodeImpl par , PathNodeImpl ret , PathNodeMid out ) {
3794
3800
exists ( ParamNodeEx p , NodeEx o , AccessPath apout |
3795
3801
pragma [ only_bind_into ] ( arg ) .getASuccessor ( ) = par and
3796
3802
pragma [ only_bind_into ] ( arg ) .getASuccessor ( ) = out and
3797
- subpaths03 ( arg , p , ret , o , apout ) and
3803
+ subpaths03 ( arg , p , localStepToHidden * ( ret ) , o , apout ) and
3804
+ not ret .isHidden ( ) and
3798
3805
par .getNodeEx ( ) = p and
3799
3806
out .getNodeEx ( ) = o and
3800
3807
out .getAp ( ) = apout
0 commit comments