Module `E_ACSL.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

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.

Install