module Mmodel_analysis:sig
..end
The data at function exit. Used for statements with no successors.
This is usually bottom, since we'll also use doStmt on Return
statements.
val reset : unit -> unit
val use_model : unit -> bool
val must_model_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
libraryval must_model_lval : ?kf:Cil_types.kernel_function ->
?stmt:Cil_types.stmt -> Cil_types.lval -> bool
Mmodel_analysis.must_model_vi
, for left-valuesval old_must_model_vi : Cil.visitor_behavior ->
?kf:Cil_types.kernel_function ->
?stmt:Cil_types.stmt -> Cil_types.varinfo -> bool
Mmodel_analysis.must_model_vi
, but assume that the given varinfo is part of the
new project generated by the given copy behavior.