package codex

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

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