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 -> (unit -> flag) -> 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