@@ -615,7 +615,16 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
615615 * A `Node` augmented with a call context (except for sinks) and an access path.
616616 * Only those `PathNode`s that are reachable from a source, and which can reach a sink, are generated.
617617 */
618- class PathNode ;
618+ class PathNode {
619+ /** Gets a textual representation of this element. */
620+ string toString ( ) ;
621+
622+ /** Gets the underlying `Node`. */
623+ Node getNode ( ) ;
624+
625+ /** Gets the location of this node. */
626+ Location getLocation ( ) ;
627+ }
619628
620629 /**
621630 * Holds if data can flow from `source` to `sink`.
@@ -639,6 +648,19 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
639648 * Holds if data can flow from some source to `sink`.
640649 */
641650 predicate flowToExpr ( DataFlowExpr sink ) ;
651+
652+ /** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
653+ predicate edges ( PathNode a , PathNode b , string key , string val ) ;
654+
655+ /** Holds if `n` is a node in the graph of data flow path explanations. */
656+ predicate nodes ( PathNode n , string key , string val ) ;
657+
658+ /**
659+ * Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
660+ * a subpath between `par` and `ret` with the connecting edges `arg -> par` and
661+ * `ret -> out` is summarized as the edge `arg -> out`.
662+ */
663+ predicate subpaths ( PathNode arg , PathNode par , PathNode ret , PathNode out ) ;
642664 }
643665
644666 /**
0 commit comments