diff options
Diffstat (limited to 'abstract/relational_apron.ml')
| -rw-r--r-- | abstract/relational_apron.ml | 10 |
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 |