Fix assertions ; fix environment equality test ; fix varialbe removal.HEADmaster

4 files changed, 35 insertions, 16 deletions

diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
index 404548c..b2d18c4 100644
--- a/abstract/environment_domain.ml
+++ b/abstract/environment_domain.ml
@@ -25,6 +25,7 @@ module type ENVIRONMENT_DOMAIN = sig
 
     (* order *)
     val subset  : t -> t -> bool
+    val eq      : t -> t -> bool
 
     (* pretty-printing *)
     val var_str : t -> id list -> string
diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index f6a6cb4..e28bf84 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -76,7 +76,8 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
         | _ -> env
         end
 
-    let rec interp_stmt env stat =
+    let rec interp_stmt_a show_asserts env stat =
+        let interp_stmt = interp_stmt_a show_asserts in
         begin match fst stat with
         | AST_block b ->
             (* remember to remove vars that have gone out of scope at the end *)
@@ -107,25 +108,30 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
             let env, u_u = unroll env 3 in
             (* widening *)
             let widen_delay = 3 in
-            let fsharp i =
-                let next_step = interp_stmt (condition cond i) body in
+            let fsharp a i =
+                let next_step = interp_stmt_a a (condition cond i) body in
                 E.join env next_step
             in
             let rec iter n i =
                 let i' =
-                    (if n < widen_delay then E.join else E.widen)
-                        i
-                        (fsharp i)
+                    if n < widen_delay
+                        then E.join i (fsharp show_asserts i)
+                        else E.widen i (fsharp false i)
                 in
-                if i = i' then i else iter (n+1) i'
+                if E.eq i i' then i else iter (n+1) i'
             in
             let x = iter 0 env in
-            let y = fix fsharp x in     (* decreasing iteration *)
-            E.join (condition (neg cond) y) u_u
+            let y = fix E.eq (fsharp false) x in     (* decreasing iteration *)
+            let z =
+                if show_asserts then
+                    (* last iteration : show real assert failures *)
+                    fsharp true y
+                else y in
+            E.join (condition (neg cond) z) u_u
         | AST_HALT -> bottom_with_vars (E.vars env)
         | AST_assert cond ->
-            if not
-                (E.is_bot (condition (neg cond) env))
+            if show_asserts && 
+                not (E.is_bot (condition (neg cond) env))
             then begin
                 Format.printf "%s: ERROR: assertion failure@."
                     (Abstract_syntax_printer.string_of_extent (snd stat));
@@ -147,6 +153,8 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
                 vars
         | _ -> assert false (* not implemented *)
         end
+
+    let interp_stmt = interp_stmt_a true
     
     let interpret prog =
         let result = List.fold_left
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 188c8bc..530b373 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -113,6 +113,16 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
                 (fun _ v -> v = V.top)
                 (fun _ a b -> V.subset a b)
                 m n
+
+    let eq a b = match a, b with
+        | Bot, Bot -> true
+        | Env m, Env n ->
+            VarMap.for_all2o
+                (fun _ _ -> false)
+                (fun _ _ -> false)
+                (fun _ a b -> a = b)
+                m n
+        | _ -> false
         
     (* pretty-printing *)
     let var_str env vars =
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