module type Data = sig
.. end
Parameters of the analysis.
type
t
Information stored at each vertex.
type
edge
Edge of the graph.
val join : t -> t -> t
Operation to join data when several paths meet.
val equal : t -> t -> bool
Equality test for data.
val analyze : edge ->
t -> t
How to analyze one edge: given an edge and the data stored at
its origin, it must compute the resulting data to be stored at
its destination.
val widening : t -> t -> t
The widening operator. fun _ x -> x
is correct and is
equivalent to not doing widening. Note that to enforce
termination, the following property should hold: for all
sequence x_0, x_1, ...
of data, the sequence defined by y_0 =
x_0; y_{i+1} = widening y_i x_i
stabilizes in finite time.