From d19afacdb5213b9ada87c9919ff8a6e05677c5d3 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 26 Nov 2020 16:55:18 +0100
Subject: [PATCH] [eacsl] Don't set RTE to off after creating a variable
---
src/plugins/e-acsl/src/code_generator/env.ml | 9 ++++-----
1 file changed, 4 insertions(+), 5 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 6372c26f3f6..cf56b61500b 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -215,9 +215,9 @@ let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env kf t ty mk_stmts =
env_stack = local_env :: tl_env }
| Varname.Block ->
let local_env =
- { block_info = new_block;
- mp_tbl = extend_tbl local_env.mp_tbl;
- rte = false (* must be already checked by mk_stmts *) }
+ { local_env with
+ block_info = new_block;
+ mp_tbl = extend_tbl local_env.mp_tbl }
in
{ env with
cpt = n;
@@ -227,8 +227,7 @@ let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env kf t ty mk_stmts =
let new_global_vars = (v, lscope) :: env.new_global_vars in
let local_env =
{ local_env with
- block_info = new_block;
- rte = false (* must be already checked by mk_stmts *) }
+ block_info = new_block }
in
{ env with
new_global_vars = new_global_vars;
--
GitLab