module Abstractions:sig
..end
type 'v
value =
| |
Single of |
| |
Struct of |
typeprecise_loc =
Precise_locs.precise_location
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 domain_functor =functor (
Value
:
Abstract.Value.External
) ->
Abstractions.leaf_domain
with type value = Value.t
type 'v
domain =
| |
Domain : |
| |
Functor : |
'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.
| *) |
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.
| *) |
type
flag =
| |
Flag : |
Abstractions.Config
for more details.val register : name:string ->
descr:string ->
?experimental:bool ->
?priority:int -> 'v abstraction -> flag
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
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)
val register_value_reduction : ('a, 'b) value_reduced_product -> unit
module type Value =sig
..end
module type S =sig
..end
module type Eva =sig
..end
val register_hook : ((module Abstractions.S) -> (module Abstractions.S)) -> unit
module Config:sig
..end
val configure : unit -> Config.t
val make : Config.t -> (module Abstractions.S)
module Legacy:S
module Default:S