Module Memory_tracking

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