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.