From b30ae45b0cecdba3b7c05962de583a06c000f70f Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 25 May 2011 13:56:17 +0000
Subject: [PATCH] [e-acsl] fix one more bug with merging of environment
---
src/plugins/e-acsl/tests/e-acsl-runtime/test_config | 2 +-
src/plugins/e-acsl/visit.ml | 6 +++---
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
index 3e7ab96b05c..28f202ce09a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
@@ -1 +1 @@
-STDOPT: +"-e-acsl-project p" +"-then-on p" +"-print" +"-val"
+STDOPT: +"-e-acsl-project p" +"-then-on p" +"-check" +"-print" +"-val"
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index a556874d14d..3c5e837604e 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -329,7 +329,7 @@ let convert_behaviors only_behaviors env behaviors =
in
Env.close_block_option pre_env,
Env.close_block_option post_env,
- Env.merge_function_vars ~from:pre_env post_env
+ Env.merge_function_vars ~from:post_env pre_env
let convert_spec only_behaviors env spec =
if spec.spec_variant <> None then Misc.not_yet "variant clause";
@@ -350,10 +350,10 @@ let convert_annotation env annot =
if l <> [] then Misc.not_yet "assertions applied only on some behaviors";
convert_named_predicate env p, None
| AStmtSpec(only_behaviors, spec) ->
- let pre_block, post_block, post_env =
+ let pre_block, post_block, new_env =
convert_spec only_behaviors env spec
in
- let env = Env.merge_function_vars ~from:post_env env in
+ let env = Env.merge_function_vars ~from:new_env env in
let env = match pre_block with
| None -> env
| Some b -> Env.add_stmt env (mkStmt ~valid_sid:true (Block b))
--
GitLab