@@ -1206,12 +1206,12 @@ module Make<
12061206 * Holds if this node is an exit node, i.e. after all stores have been performed.
12071207 *
12081208 * A local flow step should be added from this node to a data flow node representing
1209- * `sc ` inside `source`.
1209+ * `s ` inside `source`.
12101210 */
1211- predicate isExit ( SourceElement source , SummaryComponent sc , string model ) {
1211+ predicate isExit ( SourceElement source , SummaryComponentStack s , string model ) {
12121212 source = source_ and
12131213 model = model_ and
1214- state_ .isSourceOutputState ( source , TSingletonSummaryComponentStack ( sc ) , _, model )
1214+ state_ .isSourceOutputState ( source , s , _, model )
12151215 }
12161216
12171217 override predicate isHidden ( ) { not this .isEntry ( _, _) }
@@ -1460,7 +1460,7 @@ module Make<
14601460
14611461 DataFlowType getSyntheticGlobalType ( SyntheticGlobal sg ) ;
14621462
1463- DataFlowType getSourceType ( SourceBase source , SummaryComponent sc ) ;
1463+ DataFlowType getSourceType ( SourceBase source , SummaryComponentStack sc ) ;
14641464
14651465 DataFlowType getSinkType ( SinkBase sink , SummaryComponent sc ) ;
14661466 }
@@ -1543,9 +1543,9 @@ module Make<
15431543 )
15441544 or
15451545 exists ( SourceElement source |
1546- exists ( SummaryComponent sc |
1547- n .( SourceOutputNode ) .isExit ( source , sc , _) and
1548- result = getSourceType ( source , sc )
1546+ exists ( SummaryComponentStack s |
1547+ n .( SourceOutputNode ) .isExit ( source , s , _) and
1548+ result = getSourceType ( source , s )
15491549 )
15501550 or
15511551 exists ( SummaryComponentStack s , ContentSet cont |
@@ -1574,13 +1574,16 @@ module Make<
15741574 /** Gets a call that targets summarized callable `sc`. */
15751575 DataFlowCall getACall ( SummarizedCallable sc ) ;
15761576
1577+ /** Gets the enclosing callable of `source`. */
1578+ DataFlowCallable getSourceNodeEnclosingCallable ( SourceBase source ) ;
1579+
15771580 /**
1578- * Gets a data flow node corresponding to the `sc ` part of `source`.
1581+ * Gets a data flow node corresponding to the `s ` part of `source`.
15791582 *
1580- * `sc ` is typically `ReturnValue` and the result is the node that
1583+ * `s ` is typically `ReturnValue` and the result is the node that
15811584 * represents the return value of `source`.
15821585 */
1583- Node getSourceNode ( SourceBase source , SummaryComponent sc ) ;
1586+ Node getSourceNode ( SourceBase source , SummaryComponentStack s ) ;
15841587
15851588 /**
15861589 * Gets a data flow node corresponding to the `sc` part of `sink`.
@@ -1622,13 +1625,20 @@ module Make<
16221625 )
16231626 }
16241627
1625- predicate sourceLocalStep ( SourceOutputNode nodeFrom , Node nodeTo , string model ) {
1626- exists ( SummaryComponent sc , SourceElement source |
1628+ predicate sourceStep ( SourceOutputNode nodeFrom , Node nodeTo , string model , boolean local ) {
1629+ exists ( SummaryComponentStack sc , SourceElement source |
16271630 nodeFrom .isExit ( source , sc , model ) and
1628- nodeTo = StepsInput:: getSourceNode ( source , sc )
1631+ nodeTo = StepsInput:: getSourceNode ( source , sc ) and
1632+ if StepsInput:: getSourceNodeEnclosingCallable ( source ) = getNodeEnclosingCallable ( nodeTo )
1633+ then local = true
1634+ else local = false
16291635 )
16301636 }
16311637
1638+ predicate sourceLocalStep ( SourceOutputNode nodeFrom , Node nodeTo , string model ) {
1639+ sourceStep ( nodeFrom , nodeTo , model , true )
1640+ }
1641+
16321642 predicate sinkLocalStep ( Node nodeFrom , SinkInputNode nodeTo , string model ) {
16331643 exists ( SummaryComponent sc , SinkElement sink |
16341644 nodeFrom = StepsInput:: getSinkNode ( sink , sc ) and
@@ -1689,6 +1699,10 @@ module Make<
16891699 )
16901700 }
16911701
1702+ predicate sourceJumpStep ( SourceOutputNode nodeFrom , Node nodeTo ) {
1703+ sourceStep ( nodeFrom , nodeTo , _, false )
1704+ }
1705+
16921706 /**
16931707 * Holds if values stored inside content `c` are cleared at `n`. `n` is a
16941708 * synthesized summary node, so in order for values to be cleared at calls
0 commit comments