Module Fixpoint.Fixpoint_graph

Produce graphs that are suitable and efficient for fixpoint computation, notably:

• There is a distinction between the first node (that may be part of a loop) and input node (that holds the entry state of the program). This simplifes fixpoint computation algorithms, e.g. each processed node has a predecessor.

• The produced data structure is computationally and memory efficient (everything is obtained by following pointers, no hash or map is used to traverse the graph).

• Graph nodes have unique consecutively labelled integers as ids. This means that abstract states can be stored in arrays, or that Patricia trees would be well balanced in those.

module type Graph = sig ... end

Signature for the input graph. We need the vertices to be hashed for traversal. In the algorithm, we also need the first node and a function returning the successor edge and nodes.

module Make (G : Graph) : sig ... end