Module Graph__.ChaoticIteration

type 'a widening_set =
| FromWto
| Predicate of 'a -> bool

How to determine which vertices are to be considered as widening points.

  • FromWto indicates to use as widening points the heads of the weak topological ordering given as a parameter of the analysis function. This will always be a safe choice, and in most cases it will also be a good one with respect to the precision of the analysis.
  • Predicate f indicates to use f as the characteristic function of the widening set. Predicate (fun _ -> false) can be used if a widening is not needed. This variant can be used when there is a special knowledge of the graph to achieve a better precision of the analysis. For instance, if the graph happens to be the flow graph of a program, the predicate should be true for control structures heads. In any case, a condition for a safe widening predicate is that every cycle of the graph should go through at least one widening point. Otherwise, the analysis may not terminate. Note that even with a safe predicate, ensuring the termination does still require a correct widening definition.
module type G = sig ... end

Minimal graph signature for the algorithm. Sub-signature of Traverse.G.

module type Data = sig ... end

Parameters of the analysis.

module Make : functor (G : G) -> functor (D : Data with type edge = G.E.t) -> sig ... end