Module `Fixpoint_wto.Make`

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

module D : AbstractDomain with type transition = G.transition

Signature

module CLMap : sig ... end

val fixpoint_partition : 
  D.state CLMap.t ->
  G.ControlLocation.t Wto.component list ->
  D.state CLMap.t

Module Fixpoint_wto.Make

Parameters

Signature

Module `Fixpoint_wto.Make`