Module Global_context

module Global_context: sig .. end

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