Module Abstractions

module Abstractions: sig .. end

Constructions of the abstractions used by Eva.


type config = {
   cvalue : bool;
   equalities : bool;
   symbolic_locs : bool;
   bitwise : bool;
   gauges : bool;
   apron_oct : bool;
   apron_box : bool;
   polka_loose : bool;
   polka_strict : bool;
   polka_equalities : bool;
   inout : bool;
   signs : bool;
   printer : bool;
   numerors : bool;
}

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 Eva = sig .. end

Module gathering: the analysis abstractions: value, location and state abstractions;, the evaluation functions for these 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