Frama-C API - 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.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