Skip to content
Snippets Groups Projects
Commit b30ae45b authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl] fix one more bug with merging of environment

parent 2c4dbe28
No related branches found
No related tags found
No related merge requests found
STDOPT: +"-e-acsl-project p" +"-then-on p" +"-print" +"-val" STDOPT: +"-e-acsl-project p" +"-then-on p" +"-check" +"-print" +"-val"
...@@ -329,7 +329,7 @@ let convert_behaviors only_behaviors env behaviors = ...@@ -329,7 +329,7 @@ let convert_behaviors only_behaviors env behaviors =
in in
Env.close_block_option pre_env, Env.close_block_option pre_env,
Env.close_block_option post_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 = let convert_spec only_behaviors env spec =
if spec.spec_variant <> None then Misc.not_yet "variant clause"; if spec.spec_variant <> None then Misc.not_yet "variant clause";
...@@ -350,10 +350,10 @@ let convert_annotation env annot = ...@@ -350,10 +350,10 @@ let convert_annotation env annot =
if l <> [] then Misc.not_yet "assertions applied only on some behaviors"; if l <> [] then Misc.not_yet "assertions applied only on some behaviors";
convert_named_predicate env p, None convert_named_predicate env p, None
| AStmtSpec(only_behaviors, spec) -> | AStmtSpec(only_behaviors, spec) ->
let pre_block, post_block, post_env = let pre_block, post_block, new_env =
convert_spec only_behaviors env spec convert_spec only_behaviors env spec
in 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 let env = match pre_block with
| None -> env | None -> env
| Some b -> Env.add_stmt env (mkStmt ~valid_sid:true (Block b)) | Some b -> Env.add_stmt env (mkStmt ~valid_sid:true (Block b))
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment