Module Fixpoint.Fixpoint_wto

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

module type AbstractDomain = sig ... end

Signature for the analysis, which is a standard abstract interpretation (Cousot and Cousot, POPL'77)

module type Graph = sig ... end

Signature for the directed graph on which we do the fixpoint computation.

module Make (G : Graph) (D : AbstractDomain with type transition = G.transition) : sig ... end

Given a graph, an abstract domain, a WTO computation on this graph, and an initial mapping from locations to pre-state, compute the final mapping from all reachable locations to their pre-state. Note that it is better if the input node is not part of the WTO.