Merge branch 'feature/basile/95-eacsl-free-globals' into 'master'

[E-ACSL] Call E-ACSL's free function for globals in a separate functions

Closes e-acsl#105 and e-acsl#95

See merge request frama-c/frama-c!2558

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.

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

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:

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:

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

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;

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) {

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;
   }
 }

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",

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",

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;
   {

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;

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; */ ;

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_;

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; */ ;

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;

src/plugins/e-acsl/tests/bts/issue-eacsl-105.c

+/* 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;
+}

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);

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;
 }

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;
 }