Module Abstract_domain

module Abstract_domain: sig .. end

Abstract domains of the analysis.

module type Lattice = sig .. end

Lattice structure of a domain.

module type Queries = sig .. end

Queries for values stored by a domain about expressions or locations.

module type Transfer = sig .. end

Transfer function of the domain.

module type Logic = sig .. end

Logic evaluation.

module type Valuation = sig .. end

Results of an evaluation: the results of all intermediate calculation (the value of each expression and the location of each lvalue) are cached in a map.

module type S = sig .. end

Signature for the abstract domains of the analysis.

type 'a key = 'a Structure.Key_Domain.k

Keys identify abstract domains through the type of their abstract values.

type 'a structure = 'a Structure.Key_Domain.structure =

`\|`	`Void : 'a0 structure`
`\|`	`Leaf : 'a1 key -> 'a1 structure`
`\|`	`Node : 'a2 structure * 'b structure -> ('a2 * 'b) structure`

Describes the internal structure of a domain. Used internally to automatically generate efficient accessors from a generic abstract domain, which may be a combination of several domains, to a specific one.

For a simple 'leaf' domain, the structure should be:

let key = Structure.Key_Domain.create_key "name_of_the_domain";;
      let structure = Leaf key;;

Then, the key should be exported by the domain, to allow the use of the functions defined in the Abstract_domain.External interface below.

A compound domain may use the Node constructor to provide a separate access to each of its parts.

A domain can also use the Void constructor to prevent access to itself.

module type Internal = sig .. end

Internal implementation of a domain.

module type External = sig .. end

External interface of a domain, with accessors.