summaryrefslogtreecommitdiffstats
path: root/abstract/relational_apron.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/relational_apron.ml')
-rw-r--r--abstract/relational_apron.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/abstract/relational_apron.ml b/abstract/relational_apron.ml
index 926d2a9..4541b0e 100644
--- a/abstract/relational_apron.ml
+++ b/abstract/relational_apron.ml
@@ -59,9 +59,11 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct
let env2 = Environment.add env [| Var.of_string id |] [||] in
Abstract1.change_environment manager x env2 false
let rmvar x id =
+ let v = [| Var.of_string id |] in
let env = Abstract1.env x in
- let env2 = Environment.remove env [| Var.of_string id |] in
- Abstract1.change_environment manager x env2 false
+ let env2 = Environment.remove env v in
+ let y = Abstract1.forget_array manager x v false in
+ Abstract1.change_environment manager y env2 false
let vars x =
List.map Var.to_string @@
Array.to_list @@ fst @@ Environment.vars @@ Abstract1.env x
@@ -98,13 +100,11 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct
let widen = Abstract1.widening manager
let subset = Abstract1.is_leq manager
+ let eq = Abstract1.is_eq manager
let var_str x idl =
let prevars = vars x in
let rm_vars_l = List.filter (fun id -> not (List.mem id idl)) prevars in
- (* print_list "prevars" prevars;
- print_list "idl" idl;
- print_list "rm_vars_l" rm_vars_l; *)
let rm_vars = Array.of_list (List.map Var.of_string rm_vars_l) in
let xx = Abstract1.forget_array manager x rm_vars false in
let b = Buffer.create 80 in