From ee52527e608a52b4f7a5cc49e316752fbb0c944b Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 16 Mar 2020 10:12:22 +0100
Subject: [PATCH] [eacsl:codegen] Remove the moving of variables declarations
from switch to upper blocks
---
.../e-acsl/src/project_initializer/prepare_ast.ml | 13 +------------
.../e-acsl/src/project_initializer/prepare_ast.mli | 2 --
2 files changed, 1 insertion(+), 14 deletions(-)
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 411b76bf1f2..57458a56888 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -496,18 +496,7 @@ class prepare_visitor = object (self)
Annotations.iter_code_annot
(fun _ a -> self#push_post_code_annot a)
stmt;
- (* move variables declared in the body of a switch statement to the
- outer scope *)
- match stmt.skind with
- | Switch(_,sw_blk,_,_) ->
- let new_blk = Cil.mkBlock [ stmt ] in
- let new_stmt = Cil.mkStmt ~valid_sid:true (Block new_blk) in
- new_blk.blocals <- sw_blk.blocals;
- sw_blk.blocals <- [];
- has_new_stmt_in_fundec <- true;
- new_stmt
- | _ ->
- stmt)
+ stmt)
method !vfunc fundec =
Cil.DoChildrenPost
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
index db215c119ea..5237a7d39d5 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
@@ -25,8 +25,6 @@
More precisely, this module performs the following tasks:
- generating a new definition for functions with contract;
- removing term sharing;
- - moving declarations of variables declared in the bodies of switch
- statements to upper scopes;
- storing what is necessary to translate in [Keep_status];
- in case of temporal validity checks, adding the attribute "aligned" to
variables that are not sufficiently aligned. *)
--
GitLab