module Temporal:sig
..end
Transformations to detect temporal memory errors (e.g., derererence 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