diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index d9acf0cdd5023c0a28aba6e693b88f652445d086..91d9557fd95f5a5158e23339023c966eea09a8e9 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -945,8 +945,8 @@ src/plugins/occurrence/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/occurrence/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/basic_blocks.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/basic_blocks.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/global_vars.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/global_vars.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/global_context.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/global_context.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/Instantiate.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/instantiator_builder.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/instantiator_builder.mli: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/instantiate/Instantiate.mli b/src/plugins/instantiate/Instantiate.mli
index aaddb8131d05730a789bf344b1df2497912ae093..4444dd5d95bae406b65c2def46efcd16145479da 100644
--- a/src/plugins/instantiate/Instantiate.mli
+++ b/src/plugins/instantiate/Instantiate.mli
@@ -101,13 +101,12 @@ module Transform: sig
val register: (module Instantiator_builder.Generator_sig) -> unit
end
-module Global_vars:sig
- (** [get t ghost storage name] searches for an existing variable [name]. If this
- variable does not exists, it is created with the specified type [t], [ghost]
- status and [storage].
+module Global_context:sig
+ (** [get_variable name f] searches for an existing variable [name]. If this
+ variable does not exists, it is created using [f].
- The obtained varinfo does not need to be registered, it will be done by the
- transformation.
+ The obtained varinfo does not need to be registered, nor [f] needs to
+ perform the registration, it will be done by the transformation.
*)
- val get: typ -> bool -> storage -> string -> varinfo
+ val get_variable: string -> (unit -> varinfo) -> varinfo
end
diff --git a/src/plugins/instantiate/Makefile.in b/src/plugins/instantiate/Makefile.in
index 97c0b467e45c956f0aa20ea5f4c1ed956afcaa77..8635d3bace9d9077ef18361548a18fc660a56aa2 100644
--- a/src/plugins/instantiate/Makefile.in
+++ b/src/plugins/instantiate/Makefile.in
@@ -57,7 +57,7 @@ PLUGIN_EXTRA_DIRS:=\
PLUGIN_CMI :=
PLUGIN_CMO := \
options basic_blocks \
- global_vars instantiator_builder \
+ global_context instantiator_builder \
transform register \
$(SRC_STRING) \
$(SRC_STDLIB)
diff --git a/src/plugins/instantiate/global_vars.ml b/src/plugins/instantiate/global_context.ml
similarity index 94%
rename from src/plugins/instantiate/global_vars.ml
rename to src/plugins/instantiate/global_context.ml
index 379443e789b0756c3ce5ee1f423fbb628e8203b2..d28b409a52f87647dc991fddbd57582cf79928a2 100644
--- a/src/plugins/instantiate/global_vars.ml
+++ b/src/plugins/instantiate/global_context.ml
@@ -23,13 +23,12 @@
module Table = Datatype.String.Hashtbl
let table = Table.create 13
-let get typ ghost storage name =
+let get_variable name make =
if Table.mem table name then Table.find table name
else begin
try Globals.Vars.find_from_astinfo name VGlobal
with Not_found ->
- let vi = Cil.makeVarinfo ~ghost true false name typ in
- vi.vstorage <- storage ;
+ let vi = make () in
Table.add table name vi ;
vi
end
diff --git a/src/plugins/instantiate/global_vars.mli b/src/plugins/instantiate/global_context.mli
similarity index 81%
rename from src/plugins/instantiate/global_vars.mli
rename to src/plugins/instantiate/global_context.mli
index 88b711593cec3b4a4bca1a1bf53d50bd531a9552..66e600361950f022101b39f1a09e106b89eab7a4 100644
--- a/src/plugins/instantiate/global_vars.mli
+++ b/src/plugins/instantiate/global_context.mli
@@ -26,17 +26,16 @@ open Cil_types
by instantiation modules.
*)
-(** [get t ghost storage name] searches for an existing variable [name]. If this
- variable does not exists, it is created with the specified type [t], [ghost]
- status and [storage].
+(** [get_variable name f] searches for an existing variable [name]. If this
+ variable does not exists, it is created using [f].
- The obtained varinfo does not need to be registered, it will be done by the
- transformation.
+ The obtained varinfo does not need to be registered, nor [f] needs to
+ perform the registration, it will be done by the transformation.
*)
-val get: typ -> bool -> storage -> string -> varinfo
+val get_variable: string -> (unit -> varinfo) -> varinfo
(** Clears internal tables *)
val clear: unit -> unit
-(** Creates a list of global for the variables that have been created *)
+(** Creates a list of global for the elements that have been created *)
val globals: location -> global list
diff --git a/src/plugins/instantiate/stdlib/basic_alloc.ml b/src/plugins/instantiate/stdlib/basic_alloc.ml
index d2bb11bd72d056ad8fec32388893052541dbf7c0..ec54907d18f893e63fe77b54ebaa0d4dde15ecb5 100644
--- a/src/plugins/instantiate/stdlib/basic_alloc.ml
+++ b/src/plugins/instantiate/stdlib/basic_alloc.ml
@@ -61,7 +61,13 @@ let isnt_allocable ?loc size =
new_predicate { p with pred_name = [ "allocable" ]}
let heap_status () =
- let vi = Global_vars.get Cil.intType true Extern "__fc_heap_status" in
+ let name = "__fc_heap_status" in
+ let make () =
+ let vi = Cil.makeVarinfo ~ghost:true true false name Cil.intType in
+ vi.vstorage <- Extern ;
+ vi
+ in
+ let vi = Global_context.get_variable name make in
Basic_blocks.cvar_to_tvar vi
let assigns_result ?loc typ deps =
diff --git a/src/plugins/instantiate/tests/plugin/needs_globals.ml b/src/plugins/instantiate/tests/plugin/needs_globals.ml
index c76373900f59e99add35c67e7325c00d16baaabc..506da455fdb5b23a60a0d994dc2fcfb0e268c021 100644
--- a/src/plugins/instantiate/tests/plugin/needs_globals.ml
+++ b/src/plugins/instantiate/tests/plugin/needs_globals.ml
@@ -27,8 +27,13 @@ let generate_prototype function_name t =
let generate_spec needed _ _ _ =
let open Cil_types in
let open Logic_const in
- let open Instantiate.Global_vars in
- let vi = get Cil.floatType true Cil_types.Extern needed in
+ let open Instantiate.Global_context in
+ let make () =
+ let vi = Cil.makeVarinfo ~ghost:true true false needed Cil.floatType in
+ vi.vstorage <- Extern ;
+ vi
+ in
+ let vi = get_variable needed make in
let t = tvar (Cil.cvar_to_lvar vi) in
let assigns =
Cil_types.Writes [ Logic_const.new_identified_term t, From [] ]
diff --git a/src/plugins/instantiate/transform.ml b/src/plugins/instantiate/transform.ml
index 7dda9a46b9960f41b5e10742a2f5c7669b85d3b9..590ee506dbdb151d26053806b4baa26e4f15d373 100644
--- a/src/plugins/instantiate/transform.ml
+++ b/src/plugins/instantiate/transform.ml
@@ -38,7 +38,7 @@ let get_kfs () =
Hashtbl.fold (fun k v l -> (get_kfs k v) @ l) base []
let clear () =
- Global_vars.clear () ;
+ Global_context.clear () ;
let clear _ instantiator =
let module I = (val instantiator: Instantiator) in
I.clear ()
@@ -55,7 +55,7 @@ class transformer = object(self)
method! vfile _ =
let post f =
- f.globals <- (Global_vars.globals (Cil.CurrentLoc.get())) @ f.globals ;
+ f.globals <- (Global_context.globals (Cil.CurrentLoc.get())) @ f.globals ;
Ast.mark_as_changed () ;
Ast.mark_as_grown () ;
f
@@ -163,4 +163,5 @@ let compute_statuses_all_kfs () =
let transform file =
clear () ;
Visitor.visitFramacFile (new transformer) file ;
+ File.reorder_ast () ;
compute_statuses_all_kfs ()