Module Global_observer

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_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

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_clean_function : unit -> (Cil_types.varinfo * Cil_types.fundec) option

Generate a new C function containing the observers for global variable de-allocations if there are global variables.