@@ -750,6 +750,27 @@ module Private {
750
750
)
751
751
}
752
752
753
+ /**
754
+ * Holds if `p` can reach `n` in a summarized callable, using only value-preserving
755
+ * local steps. `clearsOrExpects` records whether any node on the path from `p` to
756
+ * `n` either clears or expects contents.
757
+ */
758
+ private predicate paramReachesLocal ( ParamNode p , Node n , boolean clearsOrExpects ) {
759
+ viableParam ( _, _, _, p ) and
760
+ n = p and
761
+ clearsOrExpects = false
762
+ or
763
+ exists ( Node mid , boolean clearsOrExpectsMid |
764
+ paramReachesLocal ( p , mid , clearsOrExpectsMid ) and
765
+ summaryLocalStep ( mid , n , true ) and
766
+ if
767
+ summaryClearsContent ( n , _) or
768
+ summaryExpectsContent ( n , _)
769
+ then clearsOrExpects = true
770
+ else clearsOrExpects = clearsOrExpectsMid
771
+ )
772
+ }
773
+
753
774
/**
754
775
* Holds if use-use flow starting from `arg` should be prohibited.
755
776
*
@@ -759,15 +780,11 @@ module Private {
759
780
*/
760
781
pragma [ nomagic]
761
782
predicate prohibitsUseUseFlow ( ArgNode arg , SummarizedCallable sc ) {
762
- exists ( ParamNode p , Node mid , ParameterPosition ppos , Node ret |
783
+ exists ( ParamNode p , ParameterPosition ppos , Node ret |
784
+ paramReachesLocal ( p , ret , true ) and
763
785
p = summaryArgParam0 ( _, arg , sc ) and
764
786
p .isParameterOf ( _, pragma [ only_bind_into ] ( ppos ) ) and
765
- summaryLocalStep ( p , mid , true ) and
766
- summaryLocalStep ( mid , ret , true ) and
767
787
isParameterPostUpdate ( ret , _, pragma [ only_bind_into ] ( ppos ) )
768
- |
769
- summaryClearsContent ( mid , _) or
770
- summaryExpectsContent ( mid , _)
771
788
)
772
789
}
773
790
0 commit comments