module Abstractions:sig
..end
Constructions of the abstractions used by Eva.
type
config = {
|
cvalue : |
|
equalities : |
|
symbolic_locs : |
|
bitwise : |
|
gauges : |
|
apron_oct : |
|
apron_box : |
|
polka_loose : |
|
polka_strict : |
|
polka_equalities : |
|
inout : |
|
signs : |
|
printer : |
Configuration of the abstract domain.
val default_config : config
Default configuration of Eva.
val legacy_config : config
Legacy configuration of Eva, with only the cvalue domain enabled. May be the default config as well.
val configure : unit -> config
Build a configuration according to the analysis parameters.
module type Value =sig
..end
module type S =sig
..end
Types of the abstractions of the analysis: value, location and state abstractions.
module type Standard_abstraction =Abstract_domain.Internal
with type value = Cvalue.V.t and type location = Precise_locs.precise_location
Type of abstractions that use the builtin types for values and locations
val register_dynamic_abstraction : (module Abstractions.Standard_abstraction) -> unit
val make : config -> (module Abstractions.S)
Builds the abstractions according to a configuration.
Two abstractions are instantiated at compile time: default and legacy (which may be the same).
module Legacy:S
module Default:S