`type 'a widening_set =`

1. `| FromWto`
2. `| 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 (G : G) (D : Data with type edge = G.E.t) : sig ... end`