E_ACSL.Global_observer
Observation of global variables.
Name of the function in which mk_init_function
(see below) generates the code.
Name of the function in which mk_clean_function
(see below) generates the code.
val add : Frama_c_kernel.Cil_types.varinfo -> unit
Observe the given variable if necessary.
val add_initializer :
Frama_c_kernel.Cil_types.varinfo ->
Frama_c_kernel.Cil_types.offset ->
Frama_c_kernel.Cil_types.init ->
unit
Add the initializer for the given observed variable.
val mk_init_function :
unit ->
Frama_c_kernel.Cil_types.varinfo * Frama_c_kernel.Cil_types.fundec
Generate a new C function containing the observers for global variable declarations and initializations.
val mk_clean_function :
unit ->
(Frama_c_kernel.Cil_types.varinfo * Frama_c_kernel.Cil_types.fundec) option
Generate a new C function containing the observers for global variable de-allocations if there are global variables.