module Memory_tracking:sig
..end
Compute a sound over-approximation of what left-values must be tracked by the memory model library
val reset : unit -> unit
Must be called to redo the analysis
val use_monitoring : unit -> bool
Is one variable monitored (at least)?
val must_monitor_vi : ?kf:Cil_types.kernel_function ->
?stmt:Cil_types.stmt -> Cil_types.varinfo -> bool
must_model_vi ?kf ?stmt vi
returns true
if the varinfo vi
at the given
stmt
in the given function kf
must be tracked by the memory model
library.
val must_monitor_lval : ?kf:Cil_types.kernel_function ->
?stmt:Cil_types.stmt -> Cil_types.lval -> bool
Same as must_model_vi
, for left-values
val must_monitor_exp : ?kf:Cil_types.kernel_function ->
?stmt:Cil_types.stmt -> Cil_types.exp -> bool
Same as must_model_vi
, for expressions