[eacsl:codegen] Extract global function creation

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

@@ -23,7 +23,7 @@
 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"
 
 (* Hashtable mapping global variables (as Cil_type.varinfo) to their
    initializers (if any).
@@ -59,12 +59,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 +86,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,7 +178,7 @@ 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 =

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

@@ -24,7 +24,7 @@
 
 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. *)
 

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

@@ -713,7 +713,7 @@ let inject_global_initializer file main =
     | None ->
       Kernel.warning "@[no entry point specified:@ \
                       you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
-        Global_observer.function_name;
+        Global_observer.function_init_name;
       file.globals <- file.globals @ [ cil_fct ]
   end