Module Mmodel_analysis

module Mmodel_analysis: sig .. end
Compute a sound over-approximation of what left-values must be tracked by the memory model library

The data at function exit. Used for statements with no successors. This is usually bottom, since we'll also use doStmt on Return statements.



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