Module Libabsolute.Domains

This module handle the domain environment, already equipped with some basic domains. You can add your own using the register_* functions, and combine them with the already defined ones.

module type B = sig ... end

Type of generic functors that lift a numeric domain to a boolean one

module type D1 = sig ... end

Type of domain combinator of arity 1 (e.g powerset)

module type D2 = sig ... end

Type of domain combinator of arity 2 (e.g products)

Domain environment management

val get_all : unit -> string list

collect the list of all registered domain names

val register_numeric : string -> (module Signature.Numeric) -> unit

registers a numeric domain into the list of available abstract domains

val register_boolean : string -> (module B) -> unit

registers a boolean domain into the list of available abstract domains

val register_1 : string -> (module D1) -> unit

registers a domain combinator into the list of combinators of arity 1

val register_2 : string -> (module D2) -> unit

registers a domain combinator into the list of combinators of arity 2

val parse : string -> string -> (module Signature.Domain)

builds the abstract domain corresponding to the name of the numeric representaion and boolean representation given in parameter. Domain application follows the syntax : "combinator(domain1,domain2)" where combinator has to be registered with the register_2 function (or be one of the predefined comibnator), and both domain1 and domain2 has to be registered. Useful to build a domain from a command line description

Predefined Abstract Domains

Numeric domains

Boxes with floatting point included bounds

Boxes with floatting point included or excluded bounds

Apron Boxes

Apron Polyhedra

Apron Octagons

Boolean domains

module Boolean : B

Lfts a numerical domain to a boolean one

module Utree : B

Disjunctive form with fast-precomputation for meets

Combinators

module Product : D2

Specialized Reduced Product. Corresponds to the option -d product (a,b) of AbSolute. if a constraint can be filtered exactly by the domain b, it is affected to it, otherwise it is affected to b.