Module Abstractions

module Abstractions: sig .. end

Registration and building of the analysis abstractions.


Registration of abstractions.

Dynamic registration of the abstractions to be used in an Eva analysis:

type 'v value = 
| Single of (module Abstract_value.Leaf with type t = 'v)
| Struct of 'v Abstract.Value.structure

Module types of value abstractions: either a single leaf module, or a compound of several modules described by a structure. In this last case, the structure must not contain the Void constructor.

type precise_loc = Precise_locs.precise_location 

For the moment, all domains must use precise_loc as their location abstraction, and no new location abstraction can be registered for an analysis. If you need to build a new location abstraction, please contact us.

module type leaf_domain = Abstract_domain.Leaf  with type location = precise_loc

Module type of a leaf domain over precise_loc abstraction.

module type domain_functor = functor (Value : Abstract.Value.External-> Abstractions.leaf_domain  with type value = Value.t

Module type of a functor building a leaf domain from a value abstraction.

type 'v domain = 
| Domain : (module leaf_domain with type value = 'v0) -> 'v0 domain
| Functor : (module domain_functor) -> 'a domain

Type of domain to be registered: either a leaf module with 'v as value abstraction, or a functor building a domain from any value abstraction.

type 'v abstraction = {
   values : 'v value; (*

The value abstraction.

*)
   domain : 'v domain; (*

The domain over the value abstraction.

*)
}

Abstraction to be registered.

type 't with_info = {
   name : string; (*

Name of the domain. Must be unique.

*)
   experimental : bool; (*

Is the domain experimental?

*)
   priority : int; (*

Domains with higher priority are processed first.

*)
   abstraction : 't; (*

The abstract value and the domain.

*)
}

Information about a registered abstraction.

type flag = 
| Flag : 'v abstraction with_info -> flag

Flag for an abstract domain. A domain can be programmatically enabled via its flag. See module Abstractions.Config for more details.

val register : name:string ->
descr:string ->
?experimental:bool ->
?priority:int -> 'v abstraction -> flag

Registers an abstract domain. Returns a flag for the given domain.

val dynamic_register : name:string ->
descr:string ->
?experimental:bool ->
?priority:int -> (unit -> 'v abstraction) -> unit

Register a dynamic abstraction: the abstraction is built by applying the last argument when starting an analysis, if the -eva-domains option has been set to name. See function Abstractions.register for more details.

type ('a, 'b) value_reduced_product = 'a Abstract.Value.key * 'b Abstract.Value.key * ('a -> 'b -> 'a * 'b) 

Reduced product between two value abstractions, identified by their keys.

val register_value_reduction : ('a, 'b) value_reduced_product -> unit

Register a reduction function for a value reduced product.

Types used in the engine.

module type Value = sig .. end

The external signature of value abstractions, plus the reduction function of the reduced product.

module type S = sig .. end

The three abstractions used in an Eva analysis.

module type Eva = sig .. end

The three abstractions plus an evaluation engine for these abstractions.

val register_hook : ((module Abstractions.S) -> (module Abstractions.S)) -> unit

Register a hook modifying the three abstractions after their building by the engine, before the start of each analysis.

Configuration of an analysis.

module Config: sig .. end

Configuration defining the abstractions to be used in an analysis.

val configure : unit -> Config.t

Creates the configuration according to the analysis parameters.

val make : Config.t -> (module Abstractions.S)

Builds the abstractions according to a configuration.

Two abstractions are instantiated at compile time for the default and legacy configurations (which may be the same).

module Legacy: S 
module Default: S