module Global_context:sig
..end
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:
name, list of the defintions (incl. functions)
val clear : unit -> unit
val globals : Cil_types.location -> Cil_types.global list