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:
- value abstractions, detailled in the signature;
- location abstractions, detailled in the signature;
- state abstractions, or abstract domains, detailled in .
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 ; |
|
priority : int ; |
|
values : 'v value ; |
|
domain : 'v domain ; |
}
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