Commit 2142b6f7 authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl:archi] no env for Global_observer.mk_init_function

parent d47813a3
......@@ -58,7 +58,7 @@ 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 env =
let mk_init_function () =
(* Create [__e_acsl_globals_init] function with definition
for initialization of global variables *)
let vi =
......@@ -91,7 +91,7 @@ let mk_init_function env =
(* 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] *)
let env = Env.push env in
let env = Env.push Env.empty in
(* 2-stage observation of initializers: temporal analysis must be performed
after generating observers of **all** globals *)
let env, stmts =
......@@ -133,10 +133,11 @@ let mk_init_function env =
stmts
in
(* Create a new code block with generated statements *)
let (b, env), stmts = match stmts with
let b, stmts = match stmts with
| [] -> assert false
| stmt :: stmts ->
Env.pop_and_get env stmt ~global_clear:true Env.Before, stmts
let b, _env = Env.pop_and_get env stmt ~global_clear:true Env.Before in
b, stmts
in
let stmts = Cil.mkStmt ~valid_sid:true (Block b) :: stmts in
(* Prevent multiple calls to globals_init *)
......@@ -168,7 +169,7 @@ let mk_init_function env =
let return = Cil.mkStmt ~valid_sid:true (Return (None, loc)) in
let stmts = [ init_stmt; guard; return ] in
blk.bstmts <- stmts;
vi, fundec, env
vi, fundec
let mk_delete_stmts stmts =
Varinfo.Hashtbl.fold_sorted
......
......@@ -36,7 +36,7 @@ val add: varinfo -> unit
val add_initializer: varinfo -> offset -> init -> unit
(** add the initializer for the given observed variable *)
val mk_init_function: Env.t -> varinfo * fundec * Env.t
val mk_init_function: unit -> varinfo * fundec
(** generates a new C function containing the observers for global variable
declaration and initialization *)
......@@ -45,6 +45,6 @@ val mk_delete_stmts: stmt list -> stmt list
(*
Local Variables:
compile-command: "make -C ../.."
compile-command: "make -C ../../../../.."
End:
*)
......@@ -648,10 +648,9 @@ let inject_in_global (env, main) = function
env, main
(* TODO: what about using [file.globalinit]? *)
let inject_global_initializer env file main =
let inject_global_initializer file main =
Options.feedback ~dkey ~level:2 "building global initializer.";
(* [TODO ARCHI] is env really useless? *)
let vi, fundec, _env = Global_observer.mk_init_function env in
let vi, fundec = Global_observer.mk_init_function () in
let cil_fct = GFun(fundec, Location.unknown) in
if Mmodel_analysis.use_model () then begin
match main with
......@@ -724,13 +723,13 @@ let inject_mmodel_initializer main =
Extlib.may handle_main main
let inject_in_file file =
let env, main =
let _env, main =
List.fold_left inject_in_global (Env.empty, None) file.globals
in
(* 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 env file main;
inject_global_initializer file main;
file.globals <- Logic_functions.add_generated_functions file.globals;
inject_mmodel_initializer main
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment