Module FixpointSource

Sourcemodule Fixpoint_graph : sig ... end

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

Sourcemodule Fixpoint_wto : sig ... end

Forward fixpoint computation of an abstract domain over a WTO (which is not memory-efficient).

Sourcemodule Reduce : sig ... end
Sourcemodule Regex : sig ... end

This implements a regular expression suitable for forward dataflow analysis (concat has been replaced by append), where the regular expression is represented using a term graph.

Sourcemodule Region_analysis : sig ... end
Sourcemodule Region_analysis_sig : sig ... end
Sourcemodule Wto : sig ... end

Weak topological orderings (WTOs) are a hierarchical decomposition of the a graph where each layer is topologically ordered and strongly connected components are aggregated and ordered recursively. This is a very convenient representation to describe an evaluation order to reach a fixpoint.

Sourcemodule Wto_iteration : sig ... end
Sourcemodule Wto_utils : sig ... end