From eaed2b2bcc067859f88699da14c9fb4f4a81de8a Mon Sep 17 00:00:00 2001 From: Julien Signoles <julien.signoles@cea.fr> Date: Wed, 23 Nov 2011 18:01:29 +0000 Subject: [PATCH] [e-acsl] removing inexpected debugging message --- src/plugins/e-acsl/env.ml | 1 - .../e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle | 5 ----- 2 files changed, 6 deletions(-) diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml index c60851c3471..8c0b78e2e1d 100644 --- a/src/plugins/e-acsl/env.ml +++ b/src/plugins/e-acsl/env.ml @@ -157,7 +157,6 @@ let new_var ?(global=false) env t ty mk_stmts = match t with | None -> raise No_term | Some t -> - Options.feedback "memoized %a" Term.pretty t; Term.Map.find t local_env.mpz_tbl.new_exps, env with Not_found | No_term -> do_new_var ~global env t ty mk_stmts diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle index 6728e58d32b..42f8891516e 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle @@ -1,9 +1,4 @@ -[e-acsl] memoized \old(x) -[e-acsl] memoized \old(x) -[e-acsl] memoized \old(x)-\old(x) tests/e-acsl-runtime/result.i:7:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable -[e-acsl] memoized \result -[e-acsl] memoized 0 [value] Analyzing a complete application starting at main [value] Computing initial state [value] Initial state computed -- GitLab