module Global_observer: sig
.. end
Observation of global variables.
val function_init_name : string
Name of the function in which mk_init_function
(see below) generates the
code.
val function_delete_name : string
Name of the function in which mk_delete_function
(see below) generates the
code.
val reset : unit -> unit
val is_empty : unit -> bool
val add : Cil_types.varinfo -> unit
Observe the given variable if necessary.
val add_initializer : Cil_types.varinfo -> Cil_types.offset -> Cil_types.init -> unit
Add the initializer for the given observed variable.
val mk_init_function : unit -> Cil_types.varinfo * Cil_types.fundec
Generate a new C function containing the observers for global variable
declarations and initializations.
val mk_delete_function : unit -> Cil_types.varinfo * Cil_types.fundec
Generate a new C function containing the observers for global variable
de-allocations.