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