module Abstractions:sig
..end
Registration and building of the analysis abstractions.
Dynamic registration of the abstractions to be used in an Eva analysis:
type 'v
value =
| |
Single of |
| |
Struct of |
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.
typeprecise_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 : |
| |
Functor : |
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 : |
(* | The value abstraction. | *) |
|
domain : |
(* | The domain over the value abstraction. | *) |
Abstraction to be registered.
type 't
with_info = {
|
name : |
(* | Name of the domain. Must be unique. | *) |
|
experimental : |
(* | Is the domain experimental? | *) |
|
priority : |
(* | Domains with higher priority are processed first. | *) |
|
abstraction : |
(* | The abstract value and the domain. | *) |
Information about a registered abstraction.
type
flag =
| |
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.
name
must be unique. The domain is used if the -eva-domains option
has been set to name
.descr
is a description printed in the help message of -eva-domains.experimental
is false by default. If set to true, a warning is emitted
when the domain is enabled.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. The default priority is 0.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.
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.
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