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