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.
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 = {
   name : string; (*
Name of the abstraction. Must be unique.
*)
   priority : int; (*
Domains with higher priority are processed first.
*)
   values : 'v value; (*
The value abstraction.
*)
   domain : 'v domain; (*
The domain over the value abstraction.
*)
}
Abstraction to be registered. The name of each abstraction must be unique. The priority can be any integer; domains with higher priority are always processed first. The domains currently provided by Eva have priority ranging between 1 and 19, so a priority of 0 (respectively 20) ensures that a new domain is processed after (respectively before) the classic Eva domains.
val register : enable:(unit -> bool) -> 'v abstraction -> unit
Register an abstraction. The abstraction is used in an Eva analysis only if enable () returns true at the start of the analysis.
val dynamic_register : configure:(unit -> 'a option) ->
make:('a -> 'v abstraction) -> unit
Register a dynamic abstraction: the abstraction is built by applying make (configure ()) at the start of each analysis.
type ('a, 'b) value_reduced_product = 'a Abstract.Value.key * 'b Abstract.Value.key * ('a -> 'b -> 'a * 'b) 
Value 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