Previous  Up  

Module type Bddapron.Domainlevel1.Level1

module type Level1 = sig .. end
type ('a, 'b) man
BDDAPRON Manager. The type parameter 'b indicates the underlying APRON abstract domain, as in type 'b Apron.Abstract0.t, and 'a the type of symbols.
type 'b t0
Level 0 abstract value.
type ('a, 'b) t = ('a Bddapron.Env.t, 'b t0) Bddapron.Env.value
Level 1 abstract value
val get_env : ('a, 'b) t -> 'a Bddapron.Env.t
val to_level0 : ('a, 'b) t -> 'b t0
val of_level0 : 'a Bddapron.Env.t ->
       'b t0 -> ('a, 'b) t
val size : ('a, 'b) man ->
       ('a, 'b) t -> int
Size of an abstract value.
val print : ?print_apron:((int -> string) ->
                     Format.formatter -> 'b Apron.Abstract0.t -> unit) ->
       Format.formatter -> ('a, 'b) t -> unit
Printing function
val bottom : ('a, 'b) man ->
       'a Bddapron.Env.t -> ('a, 'b) t

Basic constructor


val top : ('a, 'b) man ->
       'a Bddapron.Env.t -> ('a, 'b) t
val of_apron : ('a, 'b) man ->
       'a Bddapron.Env.t ->
       'b Apron.Abstract1.t -> ('a, 'b) t
val of_bddapron : ('a, 'b) man ->
       'a Bddapron.Env.t ->
       ('a Bddapron.Expr1.Bool.t * 'b Apron.Abstract1.t) list ->
       ('a, 'b) t

Tests


val is_bottom : ('a, 'b) man ->
       ('a, 'b) t -> bool
val is_top : ('a, 'b) man ->
       ('a, 'b) t -> bool
Emtpiness and Universality tests
val is_leq : ('a, 'b) man ->
       ('a, 'b) t ->
       ('a, 'b) t -> bool
val is_eq : ('a, 'b) man ->
       ('a, 'b) t ->
       ('a, 'b) t -> bool
Inclusion and equality tests
val to_bddapron : ('a, 'b) man ->
       ('a, 'b) t ->
       ('a Bddapron.Expr1.Bool.t * 'b Apron.Abstract1.t) list

Extraction of properties

Conversion to a disjunction of a conjunction of pair of a purely Boolean formula (without numerical constraints) and an APRON abstract value


Operations


val meet : ('a, 'b) man ->
       ('a, 'b) t ->
       ('a, 'b) t ->
       ('a, 'b) t
val join : ('a, 'b) man ->
       ('a, 'b) t ->
       ('a, 'b) t ->
       ('a, 'b) t
Meet and join
val meet_condition : ('a, 'b) man ->
       'a Bddapron.Cond.t ->
       ('a, 'b) t ->
       'a Bddapron.Expr1.Bool.t -> ('a, 'b) t
val meet_condition2 : ('a, 'b) man ->
       ('a, 'b) t ->
       'a Bddapron.Expr2.Bool.t -> ('a, 'b) t
Intersection with a Boolean expression (that may involve numerical constraints)
val assign_lexpr : ?relational:bool ->
       ?nodependency:bool ->
       ('a, 'b) man ->
       'a Bddapron.Cond.t ->
       ('a, 'b) t ->
       'a list ->
       'a Bddapron.Expr1.t list ->
       ('a, 'b) t option ->
       ('a, 'b) t
val assign_listexpr2 : ?relational:bool ->
       ?nodependency:bool ->
       ('a, 'b) man ->
       ('a, 'b) t ->
       'a list ->
       'a Bddapron.Expr2.List.t ->
       ('a, 'b) t option ->
       ('a, 'b) t
val substitute_lexpr : ('a, 'b) man ->
       'a Bddapron.Cond.t ->
       ('a, 'b) t ->
       'a list ->
       'a Bddapron.Expr1.t list ->
       ('a, 'b) t option ->
       ('a, 'b) t
val substitute_listexpr2 : ('a, 'b) man ->
       ('a, 'b) t ->
       'a list ->
       'a Bddapron.Expr2.List.t ->
       ('a, 'b) t option ->
       ('a, 'b) t
Parallel assignement/substitution of a list of variables by a list of expressions
val forget_list : ('a, 'b) man ->
       ('a, 'b) t ->
       'a list -> ('a, 'b) t
Forget (existential quantification) a list of variables
val widening : ('a, 'b) man ->
       ('a, 'b) t ->
       ('a, 'b) t ->
       ('a, 'b) t
val widening_threshold : ('a, 'b) man ->
       ('a, 'b) t ->
       ('a, 'b) t ->
       Apron.Lincons1.earray -> ('a, 'b) t
Widening
val change_environment : ('a, 'b) man ->
       ('a, 'b) t ->
       'a Bddapron.Env.t -> ('a, 'b) t

Change of environments and renaming

Change the environment (eliminate (forget) variables not belonging to the new environment, and introduce new variables)

val rename : ('a, 'b) man ->
       ('a, 'b) t ->
       ('a * 'a) list -> ('a, 'b) t
Rename a list of variables (thus changing the environment).
val unify : ('a, 'b) man ->
       ('a, 'b) t ->
       ('a, 'b) t ->
       ('a, 'b) t
Unify two abstract values on their least common environment (lce, that should exist, which implies that no variable is defined with different types in the two initial environments).

This is equivalent to change the environment to the lce, and to perform meet.