module Mmodel_analysis: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_model : unit -> bool
Is one variable monitored (at least)?
val must_model_vi : ?bhv:Cil.visitor_behavior ->
?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. If behavior bhv
is specified then assume that vi
is part
of the new project generated by the given copy behavior bhv
val must_model_lval : ?bhv:Cil.visitor_behavior ->
?kf:Cil_types.kernel_function ->
?stmt:Cil_types.stmt -> Cil_types.lval -> bool
Same as Mmodel_analysis.must_model_vi
, for left-values
val must_model_exp : ?bhv:Cil.visitor_behavior ->
?kf:Cil_types.kernel_function ->
?stmt:Cil_types.stmt -> Cil_types.exp -> bool
Same as Mmodel_analysis.must_model_vi
, for expressions