[eacsl:codegen] Remove old insertions of delete globals

src/plugins/e-acsl/src/code_generator/global_observer.ml

@@ -182,14 +182,6 @@ let mk_init_function () =
   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 *)

src/plugins/e-acsl/src/code_generator/global_observer.mli

@@ -44,9 +44,6 @@ 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. *)

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