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

1 files changed, 19 insertions, 11 deletions

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