package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Fixpoint.Fixpoint_wtoSource

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

Sourcemodule type AbstractDomain = sig ... end

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

Sourcemodule type Graph = sig ... end

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

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