From c4a24372b70180f23b7a56a81533e86ebb8509e7 Mon Sep 17 00:00:00 2001 From: Alex AUVOLAT Date: Sun, 1 Jun 2014 11:40:43 +0200 Subject: Fix assertions ; fix environment equality test ; fix varialbe removal. --- abstract/relational_apron.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'abstract/relational_apron.ml') 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 -- cgit v1.2.3