Module Global_context

module Global_context: sig .. end
The purpose of this module global definitions when it is needed by instantiation modules.


The purpose of this module global definitions when it is needed by instantiation modules.
val get_variable : string -> (unit -> Cil_types.varinfo) -> Cil_types.varinfo
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, nor f needs to perform the registration, it will be done by the transformation.

val get_logic_function : string -> (unit -> Cil_types.logic_info) -> Cil_types.logic_info
get_logic_function name f searches for an existing logic function name. If this function does not exists, it is created using f. If the logic function must be part of an axiomatic block **DO NOT** use this function, use get_logic_function_in_axiomatic.

Note that function overloading is not supported.

val get_logic_function_in_axiomatic : string ->
(unit ->
(string * Cil_types.global_annotation list) * Cil_types.logic_info list) ->
Cil_types.logic_info
get_logic_function_in_axiomatic name f searches for an existing logic function name. If this function does not exists, an axiomatic definition is created using f.

f must return:

Note that function overloading is not supported.
val clear : unit -> unit
Clears internal tables
val globals : Cil_types.location -> Cil_types.global list
Creates a list of global for the elements that have been created