Module Fixpoint

module Fixpoint_graph : sig ... end

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

module Fixpoint_wto : sig ... end

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

module Reduce : sig ... end

module 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.

module Region_analysis : sig ... end

module Region_analysis_sig : sig ... end

module 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.

module Wto_iteration : sig ... end

module Wto_utils : sig ... end