Module MkFixpoint

module MkFixpoint: sig .. end

Introduction

This module provides a generic engine for computing iteratively the solution of a fixpoint equation on a lattice.

The functor takes as argument an hypergraph module representing the system of equation. In this graph, vertices corresponds to unknown and oriented hyperedges to functions. It is assumed that hyperedges have unique destination vertex, and that associated functions are strict in each of their arguments: a bottom value in one of the argument implies that the result is empty.

Most functions of the module delivered by the functor (module type S) take as argument an object of type ('abstract,'arc) manager, where 'abstract is the type of abstract values and 'arc the type of information associated to hyperedges and computed by the fixpoint analysis. The manager of type ('abstract,arc) manager defines operations on abstract values, meaning of hyperedges, printing functions, and various options.

Real functions to be applied in the equation system are indexed by the type hedge of the graph. The result of a function application (manager.apply) is first a user-defined object of type 'arc attached to the hyperedge, and an abstract value of type 'abstract that will be joined with the current reachable value fo the destination vertex.

Module type for the fixpoint engine

module type S = sig .. end

Functor

module Make: 
functor (Graph : SHGraph.S) -> S  with module Graph = Graph