Module Fixpoint_wto.MakeSource

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.

Parameters

module G : Graph

Signature

Sourcemodule CLMap : sig ... end