Frama-C:
Plug-ins:
Libraries:

Frama-C API - Global_observer

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_clean_name : string

Name of the function in which mk_clean_function (see below) generates the code.

val reset : unit -> unit
val is_empty : unit -> bool

Observe the given variable if necessary.

Add the initializer for the given observed variable.

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.