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 is_enabled : unit -> bool
Return a boolean value indicating whether temporal analysis is enabled
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 -> 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 -> Env.t -> 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