@@ -3740,13 +3740,14 @@ private module Subpaths {
37403740 */
37413741 pragma [ nomagic]
37423742 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 ,
37443744 NodeEx out , AccessPath apout
37453745 ) {
37463746 exists ( Configuration config |
37473747 pathThroughCallable ( arg , out , _, pragma [ only_bind_into ] ( apout ) ) and
37483748 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 ( )
37503751 )
37513752 }
37523753
@@ -3780,21 +3781,27 @@ private module Subpaths {
37803781 innercc = ret .getCallContext ( ) and
37813782 sc = ret .getSummaryCtx ( ) and
37823783 ret .getConfiguration ( ) = unbindConf ( getPathNodeConf ( arg ) ) and
3783- apout = ret .getAp ( ) and
3784- not ret .isHidden ( )
3784+ apout = ret .getAp ( )
37853785 )
37863786 }
37873787
3788+ private PathNodeImpl localStepToHidden ( PathNodeImpl n ) {
3789+ n .getASuccessorImpl ( ) = result and
3790+ result .isHidden ( ) and
3791+ localFlowBigStep ( n .getNodeEx ( ) , result .getNodeEx ( ) , _, _, _, _)
3792+ }
3793+
37883794 /**
37893795 * Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
37903796 * a subpath between `par` and `ret` with the connecting edges `arg -> par` and
37913797 * `ret -> out` is summarized as the edge `arg -> out`.
37923798 */
3793- predicate subpaths ( PathNode arg , PathNodeImpl par , PathNodeMid ret , PathNodeMid out ) {
3799+ predicate subpaths ( PathNode arg , PathNodeImpl par , PathNodeImpl ret , PathNodeMid out ) {
37943800 exists ( ParamNodeEx p , NodeEx o , AccessPath apout |
37953801 pragma [ only_bind_into ] ( arg ) .getASuccessor ( ) = par and
37963802 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
37983805 par .getNodeEx ( ) = p and
37993806 out .getNodeEx ( ) = o and
38003807 out .getAp ( ) = apout
0 commit comments