@@ -615,7 +615,16 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
615
615
* A `Node` augmented with a call context (except for sinks) and an access path.
616
616
* Only those `PathNode`s that are reachable from a source, and which can reach a sink, are generated.
617
617
*/
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
+ }
619
628
620
629
/**
621
630
* Holds if data can flow from `source` to `sink`.
@@ -639,6 +648,19 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
639
648
* Holds if data can flow from some source to `sink`.
640
649
*/
641
650
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 ) ;
642
664
}
643
665
644
666
/**
0 commit comments