@@ -550,7 +550,6 @@ private predicate isRelevant(DataFlow::Node nd, DataFlow::Configuration cfg) {
550550 * either `pred` is an argument of `f` and `succ` the corresponding parameter, or
551551 * `pred` is a variable definition whose value is captured by `f` at `succ`.
552552 */
553- pragma [ noopt]
554553private predicate callInputStep ( Function f , DataFlow:: Node invk ,
555554 DataFlow:: Node pred , DataFlow:: Node succ ,
556555 DataFlow:: Configuration cfg ) {
@@ -580,6 +579,7 @@ private predicate callInputStep(Function f, DataFlow::Node invk,
580579 * Note that the summary does not take the initial step from argument to parameter
581580 * into account.
582581 */
582+ pragma [ nomagic]
583583private predicate reachableFromInput ( Function f , DataFlow:: Node invk ,
584584 DataFlow:: Node input , DataFlow:: Node nd ,
585585 DataFlow:: Configuration cfg , PathSummary summary ) {
@@ -613,20 +613,28 @@ private predicate flowThroughCall(DataFlow::Node input, DataFlow::Node invk,
613613 * Holds if `pred` may flow into property `prop` of `succ` under configuration `cfg`
614614 * along a path summarized by `summary`.
615615 */
616- private predicate storeStep ( DataFlow:: Node pred , DataFlow:: SourceNode succ , string prop ,
616+ pragma [ nomagic]
617+ private predicate storeStep ( DataFlow:: Node pred , DataFlow:: Node succ , string prop ,
617618 DataFlow:: Configuration cfg , PathSummary summary ) {
618619 basicStoreStep ( pred , succ , prop ) and
619620 summary = PathSummary:: level ( )
620621 or
621- exists ( Function f , DataFlow:: Node mid , DataFlow:: SourceNode base |
622+ exists ( Function f , DataFlow:: Node mid , DataFlow:: Node base |
622623 // `f` stores its parameter `pred` in property `prop` of a value that it returns,
623624 // and `succ` is an invocation of `f`
624625 reachableFromInput ( f , succ , pred , mid , cfg , summary ) and
625- base .hasPropertyWrite ( prop , mid ) and
626- base .flowsToExpr ( f .getAReturnedExpr ( ) )
626+ returnedPropWrite ( f , base , prop , mid )
627627 )
628628}
629629
630+ /**
631+ * Holds if `f` may return `base`, which has a write of property `prop` with right-hand side `rhs`.
632+ */
633+ predicate returnedPropWrite ( Function f , DataFlow:: SourceNode base , string prop , DataFlow:: Node rhs ) {
634+ base .hasPropertyWrite ( prop , rhs ) and
635+ base .flowsToExpr ( f .getAReturnedExpr ( ) )
636+ }
637+
630638/**
631639 * Holds if `rhs` is the right-hand side of a write to property `prop`, and `nd` is reachable
632640 * from the base of that write under configuration `cfg` (possibly through callees) along a
0 commit comments