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 : ?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
Mmodel_analysis.must_model_vi
, for left-valuesval must_model_exp : ?bhv:Cil.visitor_behavior ->
?kf:Cil_types.kernel_function ->
?stmt:Cil_types.stmt -> Cil_types.exp -> bool
Mmodel_analysis.must_model_vi
, for expressions