[eacsl:codegen] Remove the moving of variables declarations from switch to upper blocks

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

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. *)