summaryrefslogtreecommitdiff
path: root/abstract/apron_domain.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/apron_domain.ml')
-rw-r--r--abstract/apron_domain.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index ad483ec..d13afd7 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -12,6 +12,8 @@ module D : ENVIRONMENT_DOMAIN = struct
type man = Polka.loose Polka.t
let manager = Polka.manager_alloc_loose ()
+ type itv = Interval.t
+
(* abstract elements *)
type t = man Abstract1.t
@@ -87,6 +89,9 @@ module D : ENVIRONMENT_DOMAIN = struct
let vbottom x =
Abstract1.bottom manager (Abstract1.env x)
+ let var_itv x id =
+ Abstract1.bound_variable manager x (Var.of_string id)
+
(* Apply some formula to the environment *)
let rec apply_cl x (cons, rest) =
let env = Abstract1.env x in
@@ -139,5 +144,7 @@ module D : ENVIRONMENT_DOMAIN = struct
let xx = Abstract1.forget_array manager x rm_vars false in
print_all fmt xx
+ let print_itv = Interval.print
+
end