Parameter Run.G

type variable = M.key

The type of variables, or graph vertices.

type property = P.property

The type of properties.

val foreach_root : (variable -> property -> unit) -> unit

foreach_root describes the root nodes of the data flow graph as well as the properties associated with them. foreach_root contribute must call contribute x p to indicate that x is a root and that p is a lower bound on the solution at x. It may call contribute x _ several times at a single root x.

val foreach_successor : variable -> property -> (variable -> property -> unit) -> unit

foreach_successor describes the edges of the data flow graph as well as the manner in which a property at the source of an edge is transformed into a property at the target. The property at the target must of course be a monotonic function of the property at the source. Furthermore, if the property at the source is bottom then the property that is transmitted to each target should be bottom as well.