Module Temporal

module Temporal: sig .. end

Transformations to detect temporal memory errors (e.g., dereference of stale pointers).

val enable : bool -> unit

Enable/disable temporal transformations

val handle_function_parameters : 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 : Cil_types.stmt -> Env.t -> Cil_types.kernel_function -> Env.t

Update local environment (Env.t) with statements tracking temporal properties of memory blocks

val generate_global_init : Cil_types.varinfo ->
       Cil_types.offset -> Cil_types.init -> 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