summaryrefslogtreecommitdiffstats
path: root/abstract/interpret.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/interpret.ml')
-rw-r--r--abstract/interpret.ml30
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