E_ACSL.TemporalTransformations to detect temporal memory errors (e.g., dereference of stale pointers).
val handle_function_parameters :
Frama_c_kernel.Cil_types.kernel_function ->
Env.t ->
Env.thandle_function_parameters kf env updates the local environment env, according to the parameters of kf, with statements allowing to track referent numbers across function calls.
val handle_stmt :
Frama_c_kernel.Cil_types.stmt ->
Env.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Env.tUpdate local environment (Env.t) with statements tracking temporal properties of memory blocks
val generate_global_init :
Frama_c_kernel.Cil_types.varinfo ->
Frama_c_kernel.Cil_types.offset ->
Frama_c_kernel.Cil_types.init ->
Frama_c_kernel.Cil_types.stmt optionGenerate Some s, where s is a statement tracking global initializer or None if there is no need to track it