From d7a1473dbceb4152dad1c1cf842ccc7fbe92b7f2 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 4 Mar 2020 13:53:56 +0100
Subject: [PATCH] [eacsl:codegen] Extract global function creation
---
.../src/code_generator/global_observer.ml | 23 ++++++++++++-------
.../src/code_generator/global_observer.mli | 2 +-
.../e-acsl/src/code_generator/injector.ml | 2 +-
3 files changed, 17 insertions(+), 10 deletions(-)
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 8468a0177a4..a145348a031 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,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 =
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 e540f434937..64667d4f278 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.mli
+++ b/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. *)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 1939cabd184..6d202d8dfb6 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/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
--
GitLab