Module Fixpoint.Fixpoint_graphSource

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.