diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 64146494153d5145a2364601c52ed3bb2589d03e..3b8b97a86519718bc8a7591c60b1ed853a889e12 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,7 +19,13 @@
 #   configure	configure
 ###############################################################################
 
--  E-ACSL       [2020/02/09] Improve verdict messages emitted by e_acsl_assert.
+-  E-ACSL       [2020/03/10] Call E-ACSL's free functions for globals in a
+                separate function at the end of main.
+-  E-ACSL       [2020/03/10] Call `__e_acsl_memory_init` only if the memory
+                model analysis is running.
+-* E-ACSL       [2020/03/10] Fix frama-c/e-acsl#105 about misplaced
+                `__e_acsl_delete_block` in presence of gotos to return statements.
+-  E-ACSL       [2020/03/09] Improve verdict messages emitted by e_acsl_assert.
 -* E-ACSL       [2020/01/06] Fix typing bug in presence of variable-length
 	        arrays that may lead to incorrect generated code.
 -* E-ACSL       [2019/12/04] Fix bug with compiler built-ins.
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.mli b/src/plugins/e-acsl/src/code_generator/constructor.mli
index 8a64b099206bdf104d7a53fb0ccd00152f35d1e4..c12574a1ad429d810ceec67dd46553ad98606663 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.mli
+++ b/src/plugins/e-acsl/src/code_generator/constructor.mli
@@ -29,6 +29,8 @@ val mk_deref: loc:Location.t -> exp -> exp
 (** Construct a dereference of an expression. *)
 
 val mk_block: stmt -> block -> stmt
+(** Create a block statement from a block to replace a given statement.
+    Requires that (1) the block is not empty, or (2) the statement is a skip. *)
 
 (* ********************************************************************** *)
 (* E-ACSL specific code: build calls to its RTL API *)
diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.ml b/src/plugins/e-acsl/src/code_generator/global_observer.ml
index 8468a0177a43b34c12b199c5b5d8f32dab78e72c..703b4a6f6f60fca6d7f3333d31c43d3baed817b4 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/global_observer.ml
@@ -23,7 +23,8 @@
 open Cil_types
 open Cil_datatype
 
-let function_name = Functions.RTL.mk_api_name "globals_init"
+let function_init_name = Functions.RTL.mk_api_name "globals_init"
+let function_delete_name = Functions.RTL.mk_api_name "globals_delete"
 
 (* Hashtable mapping global variables (as Cil_type.varinfo) to their
    initializers (if any).
@@ -59,12 +60,14 @@ let rec literal_in_initializer env kf = function
   | CompoundInit (_, l) ->
     List.fold_left (fun env (_, i) -> literal_in_initializer env kf i) env l
 
-let mk_init_function () =
-  (* Create [__e_acsl_globals_init] function with definition
-     for initialization of global variables *)
+(* Create a global kernel function named `name`.
+   Return a triple (varinfo * fundec * kernel_function) of the created
+   global function. *)
+let mk_function name =
+  (* Create global function `name` *)
   let vi =
     Cil.makeGlobalVar ~source:true
-      function_name
+      name
       (TFun(Cil.voidType, Some [], false, []))
   in
   vi.vdefined <- true;
@@ -84,11 +87,16 @@ let mk_init_function () =
       sspec = spec }
   in
   let fct = Definition(fundec, Location.unknown) in
-  (* Create and register [__e_acsl_globals_init] as kernel
-     function *)
+  (* Create and register the function as kernel function *)
   let kf = { fundec = fct; spec = spec } in
   Globals.Functions.register kf;
   Globals.Functions.replace_by_definition spec fundec Location.unknown;
+  vi, fundec, kf
+
+let mk_init_function () =
+  (* Create and register [__e_acsl_globals_init] function with definition
+     for initialization of global variables *)
+  let vi, fundec, kf = mk_function function_init_name in
   (* Now generate the statements. The generation is done only now because it
      depends on the local variable [already_run] whose generation required the
      existence of [fundec] *)
@@ -171,16 +179,24 @@ let mk_init_function () =
   in
   let return = Cil.mkStmt ~valid_sid:true (Return (None, loc)) in
   let stmts = [ init_stmt; guard; return ] in
-  blk.bstmts <- stmts;
+  fundec.sbody.bstmts <- stmts;
   vi, fundec
 
-let mk_delete_stmts stmts =
-  Varinfo.Hashtbl.fold_sorted
-    (fun vi _l acc ->
-       if Misc.is_fc_or_compiler_builtin vi then acc
-       else Constructor.mk_delete_stmt vi :: acc)
-    tbl
-    stmts
+let mk_delete_function () =
+  (* Create and register [__e_acsl_globals_delete] function with definition
+     for de-allocation of global variables *)
+  let vi, fundec, _kf = mk_function function_delete_name in
+  (* Generate delete statements and add them to the function body *)
+  let stmts =
+    Varinfo.Hashtbl.fold_sorted
+      (fun vi _l acc ->
+         if Misc.is_fc_or_compiler_builtin vi then acc
+         else Constructor.mk_delete_stmt vi :: acc)
+      tbl
+      []
+  in
+  fundec.sbody.bstmts <- stmts;
+  vi, fundec
 
 (*
 Local Variables:
diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.mli b/src/plugins/e-acsl/src/code_generator/global_observer.mli
index e540f43493749c8ddf73450bc4a040f50fff1ada..fa18ebead123e6af2c21ddad05e397417daa1c56 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.mli
+++ b/src/plugins/e-acsl/src/code_generator/global_observer.mli
@@ -24,9 +24,12 @@
 
 open Cil_types
 
-val function_name: string
+val function_init_name: string
 (** Name of the function in which [mk_init_function] (see below) generates the
     code. *)
+val function_delete_name: string
+(** Name of the function in which [mk_delete_function] (see below) generates the
+    code. *)
 
 val reset: unit -> unit
 val is_empty: unit -> bool
@@ -41,8 +44,9 @@ val mk_init_function: unit -> varinfo * fundec
 (** Generate a new C function containing the observers for global variable
     declarations and initializations. *)
 
-val mk_delete_stmts: stmt list -> stmt list
-(** Generate the observers for global variable de-allocations. *)
+val mk_delete_function: unit -> varinfo * fundec
+(** Generate a new C function containing the observers for global variable
+    de-allocations. *)
 
 (*
 Local Variables:
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 1939cabd184c8827aac4c57c5a8b2929fa480466..40d9c3ea1a23bc99a9903513eaed31061c4a4ac6 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -268,19 +268,6 @@ let add_new_block_in_stmt env kf stmt =
       let b, env =
         Env.pop_and_get env new_stmt ~global_clear:true Env.After
       in
-      if Kernel_function.is_main kf && Mmodel_analysis.use_model () then begin
-        let stmts = b.bstmts in
-        let l = List.rev stmts in
-        match l with
-        | [] -> assert false (* at least the 'return' stmt *)
-        | ret :: l ->
-          let loc = Stmt.loc stmt in
-          let delete_stmts =
-            Global_observer.mk_delete_stmts
-              [ Constructor.mk_rtl_call ~loc "memory_clean" []; ret ]
-          in
-          b.bstmts <- List.rev l @ delete_stmts
-      end;
       let new_stmt = Constructor.mk_block stmt b in
       if not (Cil_datatype.Stmt.equal stmt new_stmt) then begin
         (* move the labels of the return to the new block in order to
@@ -329,6 +316,40 @@ let add_new_block_in_stmt env kf stmt =
     "@[new stmt (from sid %d):@ %a@]" stmt.sid Printer.pp_stmt new_stmt;
   new_stmt, env
 
+(** In the block [outer_block] in the function [kf], this function finds the
+    innermost last statement and insert the list of statements returned by
+    [last_stmts].
+    The function [last_stmts] receives an optional argument [?return_stmt] with
+    the innermost return statement if it exists. In that case the function needs
+    to return this statement as the last statement. *)
+let insert_as_last_stmts_in_innermost_block ~last_stmts kf outer_block =
+  (* Retrieve the last innermost block *)
+  let rec retrieve_innermost_last_return block =
+    let l = List.rev block.bstmts in
+    match l with
+    | [] -> block, [], None
+    | { skind = Return _ } as ret :: rest -> block, rest, Some ret
+    | { skind = Block b } :: _ -> retrieve_innermost_last_return b
+    | _ :: _ -> block, l, None
+  in
+  let inner_block, rev_content, return_stmt =
+    retrieve_innermost_last_return outer_block
+  in
+  (* Create the statements to insert *)
+  let new_stmts = last_stmts ?return_stmt () in
+  (* Move the labels from the return stmt to the stmts to insert *)
+  let new_stmts =
+    match return_stmt with
+    | Some return_stmt ->
+      let b = Cil.mkBlock new_stmts in
+      let new_stmt = Constructor.mk_block return_stmt b in
+      E_acsl_label.move kf return_stmt new_stmt;
+      [ new_stmt ]
+    | None -> new_stmts
+  in
+  (* Insert the statements as the last statements of the innermost block *)
+  inner_block.bstmts <- List.rev_append rev_content new_stmts
+
 (* visit the substmts and build the new skind *)
 let rec inject_in_substmt env kf stmt = match stmt.skind with
   | Instr instr ->
@@ -481,7 +502,21 @@ and inject_in_block (env: Env.t) kf blk =
   | [], _ :: _ | _ :: _, [] | _ :: _, _ :: _ ->
     (* [TODO] this piece of code could be improved *)
     (* de-allocate the memory blocks observing locals *)
-    let add_locals stmts =
+    let last_stmts ?return_stmt () =
+      let stmts =
+        match return_stmt with
+        | Some return_stmt ->
+          (* now that [free] stmts for [kf] have been inserted,
+             there is no more need to keep the corresponding entries in the
+             table managing them. *)
+          At_with_lscope.Free.remove_all kf;
+          (* The free statements are passed in the same order than the malloc
+             ones. In order to free the variable in the reverse order, the list
+             is reversed before appending the return statement. Moreover,
+             `rev_append` is tail recursive contrary to `append` *)
+          List.rev_append free_stmts [ return_stmt ]
+        | None -> []
+      in
       if Functions.instrument kf then
         List.fold_left
           (fun acc vi ->
@@ -494,28 +529,8 @@ and inject_in_block (env: Env.t) kf blk =
         stmts
     in
     (* select the precise location to inject these pieces of code *)
-    let rec insert_in_innermost_last_block blk = function
-      | { skind = Return _ } as ret :: ((potential_clean :: tl) as l) ->
-        (* keep the return (enclosed in a generated block) at the end;
-           preceded by clean if any *)
-        let init, tl =
-          if Kernel_function.is_main kf && Mmodel_analysis.use_model () then
-            free_stmts @ [ potential_clean; ret ], tl
-          else
-            free_stmts @ [ ret ], l
-        in
-        (* now that [free] stmts for [kf] have been inserted,
-           there is no more need to keep the corresponding entries in the
-           table managing them. *)
-        At_with_lscope.Free.remove_all kf;
-        blk.bstmts <-
-          List.fold_left (fun acc v -> v :: acc) (add_locals init) tl
-      | { skind = Block b } :: _ ->
-        insert_in_innermost_last_block b (List.rev b.bstmts)
-      | l ->
-        blk.bstmts <- List.fold_left (fun acc v -> v :: acc) (add_locals []) l
-    in
-    insert_in_innermost_last_block blk (List.rev blk.bstmts);
+    insert_as_last_stmts_in_innermost_block ~last_stmts kf blk ;
+    (* allocate the memory blocks observing locals *)
     if Functions.instrument kf then
       blk.bstmts <-
         List.fold_left
@@ -593,7 +608,7 @@ let inject_in_fundec main fundec =
   add_generated_variables_in_function env fundec;
   add_malloc_and_free_stmts kf fundec;
   (* setting main if necessary *)
-  let main = if Kernel_function.is_main kf then Some fundec else main in
+  let main = if Kernel_function.is_main kf then Some kf else main in
   Options.feedback ~dkey ~level:2 "function %a done."
     Kernel_function.pretty kf;
   env, main
@@ -670,38 +685,90 @@ let inject_in_global (env, main) = function
     ->
     env, main
 
+(* Insert [stmt_begin] as the first statement of [fundec] and insert [stmt_end] as
+   the last before [return] *)
+let surround_function_with kf fundec stmt_begin stmt_end =
+  let body = fundec.sbody in
+  (* Insert last statement *)
+  Extlib.may
+    (fun stmt_end ->
+       let last_stmts ?return_stmt () =
+         match return_stmt with
+         | Some return_stmt -> [ stmt_end; return_stmt ]
+         | None -> [ stmt_end]
+       in
+       insert_as_last_stmts_in_innermost_block ~last_stmts kf body)
+    stmt_end;
+  (* Insert first statement *)
+  body.bstmts <- stmt_begin :: body.bstmts
+
 (* TODO: what about using [file.globalinit]? *)
-let inject_global_initializer file main =
-  Options.feedback ~dkey ~level:2 "building global initializer.";
-  let vi, fundec = Global_observer.mk_init_function () in
-  let cil_fct = GFun(fundec, Location.unknown) in
-  if Mmodel_analysis.use_model () then begin
+(** Add a call to [__e_acsl_globals_init] and [__e_acsl_globals_delete] if the
+    memory model analysis is running.
+    These functions track the usage of globals if the program being analyzed. *)
+let inject_global_handler file main =
+  Options.feedback ~dkey ~level:2 "building global handler.";
+  if Mmodel_analysis.use_model () then
+    (* Create [__e_acsl_globals_init] function *)
+    let vi_init, fundec_init = Global_observer.mk_init_function () in
+    let cil_fct_init = GFun(fundec_init, Location.unknown) in
+    (* Create [__e_acsl_globals_delete] function *)
+    let vi_delete, fundec_delete = Global_observer.mk_delete_function () in
+    let cil_fct_delete = GFun(fundec_delete, Location.unknown) in
     match main with
     | Some main ->
-      let exp = Cil.evar ~loc:Location.unknown vi in
+      let mk_fct_call vi =
+        let exp = Cil.evar ~loc:Location.unknown vi in
+        let stmt =
+          Cil.mkStmtOneInstr ~valid_sid:true
+            (Call(None, exp, [], Location.unknown))
+        in
+        vi.vreferenced <- true;
+        stmt
+      in
+      let main_fundec =
+        try Kernel_function.get_definition main
+        with _ -> assert false (* by construction, the main kf has a fundec *)
+      in
       (* Create [__e_acsl_globals_init();] call *)
-      let stmt =
-        Cil.mkStmtOneInstr ~valid_sid:true
-          (Call(None, exp, [], Location.unknown))
+      let stmt_init = mk_fct_call vi_init in
+      (* Create [__e_acsl_globals_delete();] call *)
+      let stmt_delete =
+        match fundec_delete.sbody.bstmts with
+        | [] -> None
+        | _ -> Some (mk_fct_call vi_delete)
       in
-      vi.vreferenced <- true;
-      (* insert [__e_acsl_globals_init ();] as first statement of [main] *)
-      main.sbody.bstmts <- stmt :: main.sbody.bstmts;
+      (* Surround the content of main with the calls to
+         [__e_acsl_globals_init();] and [__e_acsl_globals_delete();] *)
+      surround_function_with main main_fundec stmt_init stmt_delete;
+      (* Retrieve all globals except main *)
+      let main_vi = Globals.Functions.get_vi main in
       let new_globals =
         List.fold_left
           (fun acc g -> match g with
-             | GFun({ svar = vi }, _) when Varinfo.equal vi main.svar -> acc
+             | GFun({ svar = vi }, _) when Varinfo.equal vi main_vi -> acc
              | _ -> g :: acc)
           []
           file.globals
       in
+      (* Add the globals functions and re-add main at the end *)
       let new_globals =
         let rec rev_and_extend acc = function
           | [] -> acc
           | f :: l -> rev_and_extend (f :: acc) l
         in
-        (* [__e_acsl_globals_init] and [main] at the end *)
-        rev_and_extend [ cil_fct; GFun(main, Location.unknown) ] new_globals
+        (* [main] at the end *)
+        let globals_to_add = [ GFun(main_fundec, Location.unknown) ] in
+        (* Prepend [__e_acsl_globals_delete] if not empty *)
+        let globals_to_add =
+          match fundec_delete.sbody.bstmts with
+          | [] -> globals_to_add
+          | _ -> cil_fct_delete :: globals_to_add
+        in
+        (* Prepend [__e_acsl_globals_init] *)
+        let globals_to_add = cil_fct_init :: globals_to_add in
+        (* Add these functions to the globals *)
+        rev_and_extend globals_to_add new_globals
       in
       (* add the literal string varinfos as the very first globals *)
       let new_globals =
@@ -712,41 +779,60 @@ let inject_global_initializer file main =
       file.globals <- new_globals
     | None ->
       Kernel.warning "@[no entry point specified:@ \
-                      you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
-        Global_observer.function_name;
-      file.globals <- file.globals @ [ cil_fct ]
-  end
-
-(* Add a call to [__e_acsl_memory_init] that initializes memory storage and
-   potentially records program arguments. Parameters to [__e_acsl_memory_init]
-   are addresses of program arguments or NULLs if [main] is declared without
-   arguments. *)
-let inject_mmodel_initializer main =
-  let loc = Location.unknown in
-  let nulls = [ Cil.zero loc ; Cil.zero loc ] in
-  let handle_main main =
-    let args =
-      (* record arguments only if the second has a pointer type, so argument
-         strings can be recorded. This is sufficient to capture C99 compliant
-         arguments and GCC extensions with environ. *)
-      match main.sformals with
-      | [] ->
-        (* no arguments to main given *)
-        nulls
-      | _argc :: argv :: _ when Cil.isPointerType argv.vtype ->
-        (* grab addresses of arguments for a call to the main initialization
-           function, i.e., [__e_acsl_memory_init] *)
-        List.map Cil.mkAddrOfVi main.sformals;
-      | _ :: _ ->
-        (* some non-standard arguments. *)
-        nulls
+                      you must call functions `%s', `%s', \
+                      `__e_acsl_memory_init' and `__e_acsl_memory_clean' \
+                      by yourself.@]"
+        Global_observer.function_init_name
+        Global_observer.function_delete_name;
+      let globals_func =
+        match fundec_delete.sbody.bstmts with
+        | [] -> [ cil_fct_init ]
+        | _ -> [ cil_fct_init; cil_fct_delete ]
+      in
+      file.globals <- file.globals @ globals_func
+
+(** Add a call to [__e_acsl_memory_init] and [__e_acsl_memory_clean] if the
+    memory model analysis is running.
+    [__e_acsl_memory_init] initializes memory storage and potentially records
+    program arguments. Parameters to [__e_acsl_memory_init] are addresses of
+    program arguments or NULLs if [main] is declared without arguments.
+    [__e_acsl_memory_clean] clean the memory allocated by
+    [__e_acsl_memory_init]. *)
+let inject_mmodel_handler main =
+  (* Only inject memory init and memory clean if the memory model analysis is
+     running *)
+  if Mmodel_analysis.use_model () then begin
+    let loc = Location.unknown in
+    let nulls = [ Cil.zero loc ; Cil.zero loc ] in
+    let handle_main main =
+      let fundec =
+        try Kernel_function.get_definition main
+        with _ -> assert false (* by construction, the main kf has a fundec *)
+      in
+      let args =
+        (* record arguments only if the second has a pointer type, so argument
+           strings can be recorded. This is sufficient to capture C99 compliant
+           arguments and GCC extensions with environ. *)
+        match fundec.sformals with
+        | [] ->
+          (* no arguments to main given *)
+          nulls
+        | _argc :: argv :: _ when Cil.isPointerType argv.vtype ->
+          (* grab addresses of arguments for a call to the main initialization
+             function, i.e., [__e_acsl_memory_init] *)
+          List.map Cil.mkAddrOfVi fundec.sformals;
+        | _ :: _ ->
+          (* some non-standard arguments. *)
+          nulls
+      in
+      let ptr_size = Cil.sizeOf loc Cil.voidPtrType in
+      let args = args @ [ ptr_size ] in
+      let init = Constructor.mk_rtl_call loc "memory_init" args in
+      let clean = Constructor.mk_rtl_call loc "memory_clean" [] in
+      surround_function_with main fundec init (Some clean)
     in
-    let ptr_size = Cil.sizeOf loc Cil.voidPtrType in
-    let args = args @ [ ptr_size ] in
-    let init = Constructor.mk_rtl_call loc "memory_init" args in
-    main.sbody.bstmts <- init :: main.sbody.bstmts
-  in
-  Extlib.may handle_main main
+    Extlib.may handle_main main
+  end
 
 let inject_in_file file =
   let _env, main =
@@ -755,9 +841,9 @@ let inject_in_file file =
   (* post-treatment *)
   (* extend [main] with forward initialization and put it at end *)
   if not (Global_observer.is_empty () && Literal_strings.is_empty ()) then
-    inject_global_initializer file main;
+    inject_global_handler file main;
   file.globals <- Logic_functions.add_generated_functions file.globals;
-  inject_mmodel_initializer main
+  inject_mmodel_handler main
 
 let reset_all ast =
   (* by default, do not run E-ACSL on the generated code *)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
index 9ae1f7c21ddc07f63bc7df4fb9bc58cd321fc08b..6677db53488571ae0cb179d7c6504944131f9cd8 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = -3;
   int y = 2;
   long z = 2L;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
index b5a38e3d9d550321295f8dbc1d106711339907bd..334e1f1891acd45ad6414ea94e962a4e8325adf2 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
@@ -6,7 +6,6 @@ int T2[4];
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   {
     int i = 0;
     while (i < 3) {
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
index 53a78260d27a4826b13c5b82e090bfa74cc7d5f9..007bc6daa68fc06d4f1f28ab9f26eb013b76aefb 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
@@ -570,13 +570,13 @@ int main(void)
   __retres = 0;
   __e_acsl_delete_block((void *)(t));
   __e_acsl_delete_block((void *)(& n));
-  free((void *)__gen_e_acsl_at_7);
-  free((void *)__gen_e_acsl_at_6);
-  free((void *)__gen_e_acsl_at_5);
-  free((void *)__gen_e_acsl_at_4);
-  free((void *)__gen_e_acsl_at_3);
-  free((void *)__gen_e_acsl_at_2);
   free((void *)__gen_e_acsl_at);
+  free((void *)__gen_e_acsl_at_2);
+  free((void *)__gen_e_acsl_at_3);
+  free((void *)__gen_e_acsl_at_4);
+  free((void *)__gen_e_acsl_at_5);
+  free((void *)__gen_e_acsl_at_6);
+  free((void *)__gen_e_acsl_at_7);
   __e_acsl_memory_clean();
   return __retres;
 }
@@ -706,10 +706,10 @@ void __gen_e_acsl_f(int *t)
                     "\\let m = 4; \\old(*(t + m) == -4) && \\old(*(t + (m - 4))) == 9",
                     "tests/arith/at_on-purely-logic-variables.c",8);
     __e_acsl_delete_block((void *)(& t));
-    free((void *)__gen_e_acsl_at_4);
-    free((void *)__gen_e_acsl_at_3);
-    free((void *)__gen_e_acsl_at_2);
     free((void *)__gen_e_acsl_at);
+    free((void *)__gen_e_acsl_at_2);
+    free((void *)__gen_e_acsl_at_3);
+    free((void *)__gen_e_acsl_at_4);
     return;
   }
 }
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
index 1d262fa573a8968eb3baee7c27bb2fac552e0bb5..c5a5d0cce531b902d925bd9b435b23ff6b64d963 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   long x = (long)0;
   int y = 0;
   __e_acsl_assert((int)x == y,"Assertion","main","(int)x == y",
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
index 80676d549eb3bb932c301f5540ea2683166304be..08496d44c2396e09142e025ace2d5fe9aec84610 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   int y = 1;
   __e_acsl_assert(x < y,"Assertion","main","x < y",
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
index c5a633e03505673ed4d11a1effefc365b23443d7..f8431536df11c96f3b9ef987ed96d87d51eba02a 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
@@ -85,7 +85,6 @@ int main(void)
 {
   int __retres;
   mystruct m;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 1;
   int y = 2;
   {
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
index b6a6fd8abf5cea178fca6f88b540f92a59ac141f..6b5f403f5a2f68d0bc58eed95b7ebd913c9c41cc 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
@@ -38,7 +38,6 @@ unsigned long __gen_e_acsl_f4_2(long n);
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   {
     __e_acsl_mpz_t __gen_e_acsl_f1_6;
     __e_acsl_mpz_t __gen_e_acsl__3;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
index f9c0176310cf6eec2bfd33baa69cc60ff361303a..15a95e1655951a6ae8a649d80881877aff06af4b 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
@@ -5,7 +5,6 @@ int main(void)
 {
   int __retres;
   int x;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __e_acsl_assert(1,"Assertion","main","0 == 0",
                   "tests/arith/integer_constant.i",6);
   /*@ assert 0 ≡ 0; */ ;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
index 9278b61ce9f86648b663fe7cb7ade212b1857410..7ee8de540851b4cfc13f744c22e4e0271e5e0561 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
@@ -26,7 +26,6 @@ unsigned long long my_pow(unsigned int x, unsigned int n)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   unsigned long long x = my_pow((unsigned int)2,(unsigned int)63);
   {
     __e_acsl_mpz_t __gen_e_acsl_;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
index 9426f228f9aef4d7b5589cb07889c6084df51c65..4ba24ca0879edf6173547ef7665fe0dfd3b135de 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   __e_acsl_assert(x == 0,"Assertion","main","x == 0","tests/arith/not.i",6);
   /*@ assert x ≡ 0; */ ;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
index 8d7127bbb6383e83b6e645ba2300b1e5b3f95ef5..bd22a341b9b2fb5c25072ebb4b661bfbbac0f19f 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
@@ -19,7 +19,6 @@ double avg(double a, double b)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   {
     __e_acsl_mpq_t __gen_e_acsl_;
     __e_acsl_mpq_t __gen_e_acsl__2;
diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-105.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-105.c
new file mode 100644
index 0000000000000000000000000000000000000000..23814838fe918ecb2843468da319d307ea556318
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-105.c
@@ -0,0 +1,21 @@
+/* run.config
+   COMMENT: frama-c/e-acsl#105, test for delete block before exiting the 
+    function in the presence of early return.
+*/
+
+int f() {
+  int a = 10;
+  goto lbl_1;
+
+ lbl_2:
+  /*@ assert \valid(&a); */
+  return 0;
+
+ lbl_1:
+  goto lbl_2;
+}
+
+int main(void) {
+  f();
+  return 0;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
index f9def933ef75326a30452f1c36516c48a5288ccb..66f0d9080e4c01efc18f40664b68ffd58b5a5119 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
@@ -25,7 +25,6 @@ int fact(int n)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = __gen_e_acsl_fact(5);
   __e_acsl_assert(x == 120,"Assertion","main","x == 120",
                   "tests/bts/bts1395.i",14);
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
index 869af38e287486855fd54b901886ef56a91caf92..6dddd2a40459ae418afc2b9a752964fe125984dc 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
@@ -53,6 +53,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& global_i_ptr));
+  __e_acsl_delete_block((void *)(& global_i));
+}
+
 int main(void)
 {
   int __retres;
@@ -60,8 +66,7 @@ int main(void)
   __e_acsl_globals_init();
   __gen_e_acsl_loop();
   __retres = 0;
-  __e_acsl_delete_block((void *)(& global_i_ptr));
-  __e_acsl_delete_block((void *)(& global_i));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
index 20ab35b8cb019792f609cad02946e874a71bd89e..0c35a1254beda7c48905f510b8cd0b0ae4af49f9 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
@@ -88,6 +88,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& S));
+}
+
 int main(void)
 {
   int __retres;
@@ -144,7 +149,7 @@ int main(void)
   }
   f();
   __retres = 0;
-  __e_acsl_delete_block((void *)(& S));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
index 809a47170c6359d63984dc7c997463a7d5fc9a5d..41b668706f86030c287a11992ef37b9fd3328d1c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
@@ -31,6 +31,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(_G));
+}
+
 int main(int argc, char **argv)
 {
   int __retres;
@@ -55,7 +60,7 @@ int main(int argc, char **argv)
   }
   /*@ assert \valid_read(_G[0].str); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(_G));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
index 5cd324316570b0133733102547a312cdef4c3b3f..02dcc62330216104b4a830f0aac14181c43ae900 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
@@ -21,6 +21,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& n));
+}
+
 int main(int argc, char **argv)
 {
   int __retres;
@@ -29,7 +34,7 @@ int main(int argc, char **argv)
   argc = __gen_e_acsl_atoi((char const *)n);
   a = argc;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& n));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
index 64ef82e9bf903467868e6fc87904a2957811d739..e3887d10a705e41beb1f739df200ac7a574232ae 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
@@ -5,7 +5,6 @@ long A = (long)0;
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   {
     __e_acsl_mpz_t __gen_e_acsl_A;
     __e_acsl_mpz_t __gen_e_acsl_;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
index 29d1004ec5b7ebcd3a8136c1bb4a313979aa7184..55454d5d36b67f3bfc10e27db0a1244dc5b64ba7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
@@ -24,6 +24,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& t));
+}
+
 int main(int argc, char **argv)
 {
   int tmp;
@@ -35,7 +40,7 @@ int main(int argc, char **argv)
   t.j = (_Bool)1;
   /*@ assert \initialized(&t.j); */ ;
   tmp = test(& t);
-  __e_acsl_delete_block((void *)(& t));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return tmp;
 }
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
index 8e24a58e6223bf92569de8db4eb0e67f6ee23db5..3dbfd57c93af5c2095db14eb114db36d0ea21f89 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
@@ -14,6 +14,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(t));
+}
+
 int main(void)
 {
   int __retres;
@@ -39,8 +44,8 @@ int main(void)
   }
   /*@ assert \valid(&t[0 .. 9]); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(t));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-105.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-105.c
new file mode 100644
index 0000000000000000000000000000000000000000..8ad1e10fa53fcb05e3e4ce4bc9b1fd53785a94fc
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-105.c
@@ -0,0 +1,39 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+int f(void)
+{
+  int __retres;
+  int a = 10;
+  __e_acsl_store_block((void *)(& a),(size_t)4);
+  __e_acsl_full_init((void *)(& a));
+  goto lbl_1;
+  lbl_2:
+  /*@ assert \valid(&a); */
+  {
+    int __gen_e_acsl_valid;
+    __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
+                                        (void *)(& a),(void *)0);
+    __e_acsl_assert(__gen_e_acsl_valid,"Assertion","f","\\valid(&a)",
+                    "tests/bts/issue-eacsl-105.c",11);
+  }
+  __retres = 0;
+  goto return_label;
+  lbl_1: goto lbl_2;
+  return_label: {
+                  __e_acsl_delete_block((void *)(& a));
+                  return __retres;
+                }
+}
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  f();
+  __retres = 0;
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
index cbc6c2e0d193f650e3ad3e14d969d8ba58d1518a..44cfac328f8ff8637b0acf5384c359fa86b3ea1b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   {
     int __gen_e_acsl_forall;
     int __gen_e_acsl_c;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-105.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-105.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-105.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..382eac9f065213428beb5ef5a6abbfb49a9b6194
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/issue-eacsl-105.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c
index ffb55240c93494ac3528ad961f911ea9c45767fc..7c2dc5ed4699cd1b21b3a8a1a2b331de709d4da0 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   if (x) {
     __e_acsl_assert(0,"Assertion","main","\\false",
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c
index dcfe6a61c3fd5c6f03344258a6165871a104c588..9e7f63becc8b260a7c45ea04dcb5d33350f77fdd 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c
@@ -129,7 +129,6 @@ void n(void)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __gen_e_acsl_f();
   __gen_e_acsl_g();
   __gen_e_acsl_h();
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c
index e942d64b232a327b604995b2a34c219ae3ed5553..ab2bc7b703821eac9e38b82846f04b971497d3c5 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c
@@ -16,6 +16,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& P));
+  __e_acsl_delete_block((void *)(& G));
+}
+
 int main(void)
 {
   int __retres;
@@ -67,9 +73,8 @@ int main(void)
     G ++;
   }
   __retres = 0;
-  __e_acsl_delete_block((void *)(& P));
-  __e_acsl_delete_block((void *)(& G));
   __e_acsl_delete_block((void *)(& q));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c
index 226d6482951d71ee138e647e9fa4a65417894720..803e14a2914f164781f4cd2324420ffc2567e370 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   {
     int i = 0;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c
index c364fb15de4e27537de95c6d4e448d0b83823e5b..06a5de92573cd1f63bb730d2872ce69f3432a319 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c
@@ -40,7 +40,6 @@ int __gen_e_acsl_main(void)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __retres = __gen_e_acsl_main();
   __e_acsl_assert(X == 3,"Postcondition","main","X == 3",
                   "tests/constructs/labeled_stmt.i",7);
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c
index 72434006bf47588df548c0678e4b112bc3dc58b7..b9ba06467be864939e8f22b5f52bfe826b1b814e 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   int y = 1;
   {
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c
index 2626d70b85c3bea55d62ce250c25c032162e59f1..879d1ee52a8ea1608999651843b866fc15f8f381 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c
@@ -183,7 +183,6 @@ void unnatural_loop(void)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   simple_loop();
   nested_loops();
   unnatural_loop();
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c
index 9411fb1ecd898231338a95b44f172fd3e1cce1e2..252046ac3c885a76d1db75b9e766725b2a12340b 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   int y = 1;
   __e_acsl_assert(x < y,"Assertion","main","x < y",
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c
index 88919141b53aa7d6efcdc5340f0a56d232ca002d..6b0f6fcf6b200810222c7a03b36bd41a2d2b6526 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c
@@ -35,7 +35,6 @@ int h(void)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __gen_e_acsl_f(1);
   __gen_e_acsl_g(Y);
   __gen_e_acsl_h();
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c
index 0fc68d324f2eb5da8ce6809cee84eff4ef73e042..b9942c443b734d7b8125e9eb9632e5a9e0a1cd03 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   int y = 2;
   /*@ ensures x ≡ 1; */
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c
index f8a614b4c4852a3de940e41309b9bd66939114b8..243f60598a1d7058fdac1047fc7513c4dea1bc85 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   x ++;
   __e_acsl_assert(1,"Assertion","main","\\true","tests/constructs/true.i",8);
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c
index 7b74563fa1e006d1c03eab9cb71b0c58329ff459..92e02166357ca38676b0a54bdfe18e6b4a1015b6 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c
@@ -5,7 +5,6 @@ typedef unsigned char uint8;
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   uint8 x = (unsigned char)0;
   __e_acsl_assert((int)x == 0,"Assertion","main","x == 0",
                   "tests/constructs/typedef.i",9);
diff --git a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
index 09509e5c90ae60ba35b72a502589d90688aef2d7..6657c1ae8ee2ab44422f5fe7bf30ed3f45503d99 100644
--- a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
@@ -102,7 +102,6 @@ int main(void)
 {
   int __retres;
   int found;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   {
     int i = 0;
     while (i < 10) {
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
index a96c903d115bcde7976d3b96ab1b10bcdd5c5d73..ca3a611c9bd240c6dba0d59cbea332b76cbe4f44 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
@@ -57,6 +57,20 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& f));
+  __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
+  __e_acsl_delete_block((void *)(__fc_tmpnam));
+  __e_acsl_delete_block((void *)(& __fc_p_fopen));
+  __e_acsl_delete_block((void *)(__fc_fopen));
+  __e_acsl_delete_block((void *)(& stdin));
+  __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
+  __e_acsl_delete_block((void *)(random48_counter));
+  __e_acsl_delete_block((void *)(& __fc_random48_init));
+  __e_acsl_delete_block((void *)(& __fc_rand_max));
+}
+
 int main(void)
 {
   int __retres;
@@ -72,18 +86,9 @@ int main(void)
   /*@ assert &x ≡ &x; */ ;
   __e_acsl_full_init((void *)(& __retres));
   __retres = 0;
-  __e_acsl_delete_block((void *)(& f));
-  __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
-  __e_acsl_delete_block((void *)(__fc_tmpnam));
-  __e_acsl_delete_block((void *)(& __fc_p_fopen));
-  __e_acsl_delete_block((void *)(__fc_fopen));
-  __e_acsl_delete_block((void *)(& stdin));
-  __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
-  __e_acsl_delete_block((void *)(random48_counter));
-  __e_acsl_delete_block((void *)(& __fc_random48_init));
-  __e_acsl_delete_block((void *)(& __fc_rand_max));
   __e_acsl_delete_block((void *)(& x));
   __e_acsl_delete_block((void *)(& __retres));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
index 721e12502219c7738e2547f6a0bd1ac1f5a6722b..dc901aa064e92b92e00e8c4b63a5fb05f813fca9 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = -3;
   int y = 2;
   long z = 2L;
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
index f47d15dc1de8409ff9909b8e03349666e21302b8..25a8fe984219cdd86055a1fc7173d91303cc1530 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
@@ -83,7 +83,6 @@ int main(void)
 {
   int __retres;
   mystruct m;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 1;
   int y = 2;
   {
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
index 6f888df6d065d78c22c954269449c6aa082a292c..9f45f3d678f16d88ce64d3a27351bafe295429bc 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
@@ -16,6 +16,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& PA));
+  __e_acsl_delete_block((void *)(A));
+}
+
 int main(void)
 {
   int __retres;
@@ -311,8 +317,6 @@ int main(void)
   }
   /*@ assert \base_addr(q) ≡ \base_addr(qd); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& PA));
-  __e_acsl_delete_block((void *)(A));
   __e_acsl_delete_block((void *)(& qd));
   __e_acsl_delete_block((void *)(& q));
   __e_acsl_delete_block((void *)(& pd));
@@ -322,6 +326,7 @@ int main(void)
   __e_acsl_delete_block((void *)(& l));
   __e_acsl_delete_block((void *)(& pa));
   __e_acsl_delete_block((void *)(a));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
index 4f0f4366d63a92caa4c16a1376aef65e6e0c0fdd..4cbe891d458c6fac7738d2ce38d0b5fc3b5e6a98 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
@@ -22,6 +22,13 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& ZERO));
+  __e_acsl_delete_block((void *)(& PA));
+  __e_acsl_delete_block((void *)(A));
+}
+
 int main(void)
 {
   int __retres;
@@ -238,9 +245,6 @@ int main(void)
   }
   /*@ assert \block_length(q) ≡ size; */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& ZERO));
-  __e_acsl_delete_block((void *)(& PA));
-  __e_acsl_delete_block((void *)(A));
   __e_acsl_delete_block((void *)(& q));
   __e_acsl_delete_block((void *)(& p));
   __e_acsl_delete_block((void *)(& pi));
@@ -249,6 +253,7 @@ int main(void)
   __e_acsl_delete_block((void *)(& pa));
   __e_acsl_delete_block((void *)(a));
   __e_acsl_delete_block((void *)(& zero));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
index a839a6888e5457bdd352c8bbff5536f6cc609bd6..3871a01e451cfe6dde011661ac2b0b4942854639 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
@@ -15,6 +15,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& B));
+}
+
 int main(int argc, char **argv)
 {
   int __retres;
@@ -151,11 +156,11 @@ int main(int argc, char **argv)
   }
   /*@ assert ¬\valid(pmax - diff); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& B));
   __e_acsl_delete_block((void *)(& pmax));
   __e_acsl_delete_block((void *)(& pmin));
   __e_acsl_delete_block((void *)(& b));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
index e10793f41018677657e111efbaf3f8b81307a83e..a5c535378151910cf595a16301c5ac72aa331ff9 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
@@ -65,6 +65,17 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(_G));
+  __e_acsl_delete_block((void *)(& _E));
+  __e_acsl_delete_block((void *)(_D));
+  __e_acsl_delete_block((void *)(& _C));
+  __e_acsl_delete_block((void *)(& _B));
+  __e_acsl_delete_block((void *)(_A));
+  __e_acsl_delete_block((void *)(& _F));
+}
+
 int main(int argc, char **argv)
 {
   int __retres;
@@ -176,13 +187,7 @@ int main(int argc, char **argv)
                   "tests/memory/compound_initializers.c",43);
   /*@ assert _G[0].num ≡ 99; */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(_G));
-  __e_acsl_delete_block((void *)(& _E));
-  __e_acsl_delete_block((void *)(_D));
-  __e_acsl_delete_block((void *)(& _C));
-  __e_acsl_delete_block((void *)(& _B));
-  __e_acsl_delete_block((void *)(_A));
-  __e_acsl_delete_block((void *)(& _F));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
index f8a0d9b78f7f2b704c58c6b33afcdaaebc45ad89..cc458e4e367b7f4f52387e3d42d727f7ff9f4df6 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
@@ -13,6 +13,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& errno));
+}
+
 int main(int argc, char const **argv)
 {
   int __retres;
@@ -38,8 +43,8 @@ int main(int argc, char const **argv)
   }
   /*@ assert \valid(p); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& errno));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
index 57d0968b67750997726a2d69abdb2203f2206f79..6504639acc77d78fee02adba6c18807b8d3d0c27 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
@@ -13,6 +13,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(array));
+}
+
 int main(void)
 {
   int __retres;
@@ -75,8 +80,8 @@ int main(void)
   }
   /*@ assert ¬\freeable(&array[5]); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(array));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
index 21e0d8d49e93362922685b0c1538a1026d24bedf..dcd56fb12c71d3ca2e9cc8fa528992df29cc0cd0 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
@@ -9,7 +9,6 @@ void function(int a, int b, int c, int d)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int w = 0;
   int x = 1;
   int y = 2;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
index ac4c3251956faf3ce1a4ee25379caa79d892b195..d5c1542ac4f7e43c2a39612fd1f6f8b8205fc76c 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
@@ -13,6 +13,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& a));
+}
+
 int main(void)
 {
   int __retres;
@@ -34,8 +39,8 @@ int main(void)
   }
   /*@ assert \initialized(b); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& a));
   __e_acsl_delete_block((void *)(& b));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
index 97f4520a88aef0c989249eab9a2abc1c9c02cb2f..e3a9201614e27d12a529b3bf3b659e3654f02192 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
@@ -16,6 +16,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& b));
+  __e_acsl_delete_block((void *)(& a));
+}
+
 int main(void)
 {
   int __retres;
@@ -45,10 +51,9 @@ int main(void)
   }
   /*@ assert \initialized(p); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& b));
-  __e_acsl_delete_block((void *)(& a));
   __e_acsl_delete_block((void *)(& q));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
index c426b1e926591f79e583da1089d6e600480e80dc..026e4bbef144f7d8a119f8d9d5fee687fb3f4dd6 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
@@ -16,6 +16,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& B));
+  __e_acsl_delete_block((void *)(& A));
+}
+
 int main(void)
 {
   int __retres;
@@ -352,8 +358,6 @@ int main(void)
   dup[0] = 1;
   dup[0] = 1;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& B));
-  __e_acsl_delete_block((void *)(& A));
   __e_acsl_delete_block((void *)(d));
   __e_acsl_delete_block((void *)(c));
   __e_acsl_delete_block((void *)(& r));
@@ -361,6 +365,7 @@ int main(void)
   __e_acsl_delete_block((void *)(& a));
   __e_acsl_delete_block((void *)(& q));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
index 3dbfb76f1f0296ca96e263e5bd18e3cacd55021f..74ba7f26de69c765049127433fb50106aa2b6dfd 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
@@ -82,6 +82,15 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& l_str));
+  __e_acsl_delete_block((void *)(& s_str));
+  __e_acsl_delete_block((void *)(& S2));
+  __e_acsl_delete_block((void *)(& S));
+  __e_acsl_delete_block((void *)(& T));
+}
+
 int main(void)
 {
   int __retres;
@@ -138,12 +147,8 @@ int main(void)
   s_str ++;
   l_str ++;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& l_str));
-  __e_acsl_delete_block((void *)(& s_str));
-  __e_acsl_delete_block((void *)(& S2));
-  __e_acsl_delete_block((void *)(& S));
-  __e_acsl_delete_block((void *)(& T));
   __e_acsl_delete_block((void *)(& SS));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
index 2556be7d0248ecfe121130a372fa8be4fa7cbe03..1f7424a1ec1eae755ed5ec0b6ae0b5c396c36c94 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
@@ -22,6 +22,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& p));
+  __e_acsl_delete_block((void *)(& X));
+}
+
 int main(void)
 {
   int __retres;
@@ -29,8 +35,7 @@ int main(void)
   __e_acsl_globals_init();
   f();
   __retres = 0;
-  __e_acsl_delete_block((void *)(& p));
-  __e_acsl_delete_block((void *)(& X));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
index ba7b47ef1efb3dcf236f93b079d608c747538631..02d31514dd514a5bfd5f727e2be47391a94815c2 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __e_acsl_assert((void *)0 == (void *)0,"Assertion","main",
                   "\\null == (void *)0","tests/memory/null.i",6);
   /*@ assert \null ≡ (void *)0; */ ;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
index 5c92ba3302262ac4dafabd204b8630980d5cac1b..4ce316ea42cfb59cd90e1929990019505f16440e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
@@ -16,6 +16,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& PA));
+  __e_acsl_delete_block((void *)(A));
+}
+
 int main(void)
 {
   int __retres;
@@ -208,14 +214,13 @@ int main(void)
   }
   /*@ assert \offset(q) ≡ sizeof(long) * 7; */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& PA));
-  __e_acsl_delete_block((void *)(A));
   __e_acsl_delete_block((void *)(& q));
   __e_acsl_delete_block((void *)(& p));
   __e_acsl_delete_block((void *)(& pi));
   __e_acsl_delete_block((void *)(& pl));
   __e_acsl_delete_block((void *)(& l));
   __e_acsl_delete_block((void *)(a));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
index 1af62be53369d574c402c31fd5c59bb7c192637c..e6f639fa93586a5740844dada0ba1163d4c1fc34 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
@@ -8,7 +8,6 @@ enum bool {
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __e_acsl_assert(1,"Assertion","main","\'c\' == \'c\'",
                   "tests/memory/other_constants.i",10);
   /*@ assert 'c' ≡ 'c'; */ ;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
index 91f376c34796a2f330bac280083e03fb8e6a9e5b..e021ea6783c863b45d6d1911bf9f1b6ba0536757 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
@@ -32,6 +32,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& B));
+  __e_acsl_delete_block((void *)(& A));
+}
+
 int main(void)
 {
   int __retres;
@@ -60,10 +66,9 @@ int main(void)
   /*@ assert \initialized(&x); */ ;
   g(x,y);
   __retres = 0;
-  __e_acsl_delete_block((void *)(& B));
-  __e_acsl_delete_block((void *)(& A));
   __e_acsl_delete_block((void *)(& y));
   __e_acsl_delete_block((void *)(& x));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
index 0439ae760d247323b99500285a5e4fa68a30ba09..7920e6b98d14aa615660abce4145ecb3cb3ea401 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   x ++;
   __e_acsl_assert(1,"Assertion","main","sizeof(int) == sizeof(x)",
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
index f9b0f156e87318aee8dedbc78a7ba7938e883a35..49ec6cf163ec5ba0edfad147a4fa237e95bb0678 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
@@ -16,6 +16,13 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& stdout));
+  __e_acsl_delete_block((void *)(& stdin));
+  __e_acsl_delete_block((void *)(& stderr));
+}
+
 int main(void)
 {
   int __retres;
@@ -46,9 +53,7 @@ int main(void)
   }
   /*@ assert \valid(__fc_stdout); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& stdout));
-  __e_acsl_delete_block((void *)(& stdin));
-  __e_acsl_delete_block((void *)(& stderr));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
index 70735ca3898ab082aed8f735f4d730a7589ad0fc..38b803a26a325b0b7f87db4a9117ad74d7359762 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
@@ -137,6 +137,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& Z));
+  __e_acsl_delete_block((void *)(& X));
+}
+
 int main(void)
 {
   int __retres;
@@ -521,13 +527,12 @@ int main(void)
   /*@ assert \valid(&Z); */ ;
   g();
   __retres = 0;
-  __e_acsl_delete_block((void *)(& Z));
-  __e_acsl_delete_block((void *)(& X));
   __e_acsl_delete_block((void *)(& n));
   __e_acsl_delete_block((void *)(& d));
   __e_acsl_delete_block((void *)(& c));
   __e_acsl_delete_block((void *)(& b));
   __e_acsl_delete_block((void *)(& a));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
index 0678e6d623602828c51fde50fe13cb6ec0b5c6e2..dcc566b58e8566c1d56d8ef15dbf2bd961ea6918 100644
--- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
@@ -24,7 +24,6 @@ int incr(int x)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int i = __gen_e_acsl_f(2);
   __retres = 0;
   return __retres;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
index ca59330238b1a3b7d7df6ab8aa7a29843acc1581..f2c564d40b49843100e080bb245424a1ef3e40e1 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
@@ -58,6 +58,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(Vertices2));
+  __e_acsl_delete_block((void *)(Vertices));
+}
+
 int main(int argc, char const **argv)
 {
   int __retres;
@@ -105,13 +111,12 @@ int main(int argc, char const **argv)
   __e_acsl_temporal_save_nblock_parameter((void *)(triple_vertices2[0]),0U);
   abe_matrix(triple_vertices2[0]);
   __retres = 0;
-  __e_acsl_delete_block((void *)(Vertices2));
-  __e_acsl_delete_block((void *)(Vertices));
   __e_acsl_delete_block((void *)(triple_vertices2));
   __e_acsl_delete_block((void *)(triple_vertices));
   __e_acsl_delete_block((void *)(vertices3));
   __e_acsl_delete_block((void *)(vertices2));
   __e_acsl_delete_block((void *)(vertices));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
index 4a0750a1833961e9cc5ed7bee0ea397cba57e6e2..6ce50be381f69a319c1fed912c25b458a733a14b 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
@@ -18,6 +18,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& foo));
+}
+
 int main(int argc, char const **argv)
 {
   int __retres;
@@ -61,10 +66,10 @@ int main(int argc, char const **argv)
   /*@ assert \valid(q); */ ;
   __retres = 0;
   __e_acsl_delete_block((void *)(& argc));
-  __e_acsl_delete_block((void *)(& foo));
   __e_acsl_delete_block((void *)(& fp));
   __e_acsl_delete_block((void *)(& q));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
index d1c0cc7c58f5b37b821cdef493dea621b1a313f6..1a223bf90f4bb66628d86a49641066fc554af8cc 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
@@ -110,6 +110,16 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(descs2));
+  __e_acsl_delete_block((void *)(& l_desc2));
+  __e_acsl_delete_block((void *)(descs));
+  __e_acsl_delete_block((void *)(& l_desc));
+  __e_acsl_delete_block((void *)(extra_lbits));
+  __e_acsl_delete_block((void *)(strings));
+}
+
 int main(int argc, char const **argv)
 {
   int __retres;
@@ -193,13 +203,8 @@ int main(int argc, char const **argv)
   }
   /*@ assert \valid_read(*p); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(descs2));
-  __e_acsl_delete_block((void *)(& l_desc2));
-  __e_acsl_delete_block((void *)(descs));
-  __e_acsl_delete_block((void *)(& l_desc));
-  __e_acsl_delete_block((void *)(extra_lbits));
-  __e_acsl_delete_block((void *)(strings));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
index b6341802859d40a4fa7482e3bd7206f0c98f8bd3..9ccb27aa258ca9cd5f58e030f4523d3535aec27f 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
@@ -106,6 +106,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(Str));
+  __e_acsl_delete_block((void *)(Strings));
+}
+
 int main(int argc, char const **argv)
 {
   int __retres;
@@ -411,8 +417,6 @@ int main(int argc, char const **argv)
   __e_acsl_temporal_save_nblock_parameter((void *)(& descs2[1].desc),0U);
   build_tree(& descs2[1].desc);
   __retres = 0;
-  __e_acsl_delete_block((void *)(Str));
-  __e_acsl_delete_block((void *)(Strings));
   __e_acsl_delete_block((void *)(descs2));
   __e_acsl_delete_block((void *)(& l_desc2));
   __e_acsl_delete_block((void *)(descs));
@@ -422,6 +426,7 @@ int main(int argc, char const **argv)
   __e_acsl_delete_block((void *)(str));
   __e_acsl_delete_block((void *)(& p));
   __e_acsl_delete_block((void *)(strings));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }