@@ -669,21 +669,18 @@ private predicate reachableFromSource(DataFlow::Node nd, DataFlow::Configuration
669669
670670/**
671671 * Holds if `nd` can be reached from a source under `cfg`, and in turn a sink is
672- * reachable from `nd`. The path from the source to `nd` is summarized by `summary1`,
673- * the path from `nd` to the sink is summarized by `summary2`.
672+ * reachable from `nd`, where the path from the source to `nd` is summarized by `summary`.
674673 */
675674private predicate onPath ( DataFlow:: Node nd , DataFlow:: Configuration cfg ,
676- PathSummary summary1 , PathSummary summary2 ) {
677- reachableFromSource ( nd , cfg , summary1 ) and
678- isSink ( nd , cfg , summary1 .getEndLabel ( ) ) and
679- not cfg .isBarrier ( nd ) and
680- summary2 = PathSummary:: level ( )
675+ PathSummary summary ) {
676+ reachableFromSource ( nd , cfg , summary ) and
677+ isSink ( nd , cfg , summary .getEndLabel ( ) ) and
678+ not cfg .isBarrier ( nd )
681679 or
682- exists ( DataFlow:: Node mid , PathSummary newSummary , PathSummary oldSummary |
683- onPath ( mid , cfg , _, oldSummary ) and
684- flowStep ( nd , cfg , mid , newSummary ) and
685- reachableFromSource ( nd , cfg , summary1 ) and
686- summary2 = oldSummary .prepend ( newSummary )
680+ exists ( DataFlow:: Node mid , PathSummary stepSummary |
681+ reachableFromSource ( nd , cfg , summary ) and
682+ flowStep ( nd , cfg , mid , stepSummary ) and
683+ onPath ( mid , cfg , summary .append ( stepSummary ) )
687684 )
688685}
689686
@@ -692,7 +689,7 @@ private predicate onPath(DataFlow::Node nd, DataFlow::Configuration cfg,
692689 */
693690private newtype TPathNode =
694691 MkPathNode ( DataFlow:: Node nd , DataFlow:: Configuration cfg , PathSummary summary ) {
695- onPath ( nd , cfg , summary , _ )
692+ onPath ( nd , cfg , summary )
696693 }
697694
698695/**
0 commit comments