E_ACSL.Temporal
Transformations 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.t
handle_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.t
Update 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 option
Generate Some s
, where s
is a statement tracking global initializer or None
if there is no need to track it