module L:Wp.Sigs.LogicSemantics
with module M = M
module M:Wp.Sigs.Model
typeloc =
M.loc
typevalue =
M.loc Wp.Sigs.value
typelogic =
M.loc Wp.Sigs.logic
typeregion =
M.loc Wp.Sigs.region
typeresult =
M.loc Wp.Sigs.result
typesigma =
M.Sigma.t
Frames are compilation environment for ACSL. A frame typically
manages the current function, formal paramters, the memory environments
at different labels and the \result
and \exit_status
values.
The frame also holds the gamma environment responsible for accumulating typing constraints, and the pool for generating fresh logic variables.
Notice that a frame
is not responsible for holding the environment
at label Here
, since this is managed by a specific compilation
environment, see Wp.Sigs.LogicSemantics.env
below.
type
frame
val pp_frame : Format.formatter -> frame -> unit
val get_frame : unit -> frame
val in_frame : frame -> ('a -> 'b) -> 'a -> 'b
Lang.gamma
and Lang.pool
contexts are also set accordingly.val mem_at_frame : frame ->
Wp.Clabels.c_label -> sigma
Here
.val set_at_frame : frame ->
Wp.Clabels.c_label -> sigma -> unit
val mem_frame : Wp.Clabels.c_label -> sigma
mem_at_frame
but for the current frame.val mk_frame : ?kf:Cil_types.kernel_function ->
?result:result ->
?status:Wp.Lang.F.var ->
?formals:value Cil_datatype.Varinfo.Map.t ->
?labels:sigma Wp.Clabels.LabelMap.t ->
?descr:string -> unit -> frame
val local : descr:string -> frame
val frame : Cil_types.kernel_function -> frame
type
call
val call : ?result:M.loc ->
Cil_types.kernel_function ->
value list -> call
result
is specified, the called function will stored its result
at the provided location in the current frame (the callee).val call_pre : sigma ->
call ->
sigma -> frame
val call_post : sigma ->
call ->
sigma Wp.Sigs.sequence -> frame
val return : unit -> Cil_types.typ
val result : unit -> result
val status : unit -> Wp.Lang.F.var
val guards : frame -> Wp.Lang.F.pred list
type
env
Here
.
Remark: don't confuse the current memory state with the
memory state at label Here
. The current memory state is the one
we have at hand when compiling a term or a predicate. Hence, inside
\at(e,L)
the current memory state when compiling e
is the one at L
.
val mk_env : ?here:sigma ->
?lvars:Cil_types.logic_var list -> unit -> env
Current and Here
memory points are initialized to ~here
, if
provided.
The logic variables stand for
formal parameters of ACSL logic function and ACSL predicates.
val current : env -> sigma
move
before.val move_at : env ->
sigma -> env
Here
memory state.
This memory state becomes also the new current one.val mem_at : env ->
Wp.Clabels.c_label -> sigma
Here
and the current frame
otherwize.val env_at : env ->
Wp.Clabels.c_label -> env
e
inside
\at(e,L)
ACSL construct.val lval : env -> Cil_types.term_lval -> Cil_types.typ * M.loc
val term : env -> Cil_types.term -> Wp.Lang.F.term
val pred : Wp.Sigs.polarity ->
env -> Cil_types.predicate -> Wp.Lang.F.pred
val region : env ->
unfold:bool -> Cil_types.term -> region
~unfold:true
, compound memory locations are expanded
field-by-field.val assigned_of_lval : env ->
unfold:bool -> Cil_types.lval -> region
val assigned_of_froms : env ->
unfold:bool -> Cil_types.from list -> region
val assigned_of_assigns : env ->
unfold:bool -> Cil_types.assigns -> region option
None
means everyhting is assigned.val val_of_term : env -> Cil_types.term -> Wp.Lang.F.term
term
above but reject any set of locations.val loc_of_term : env -> Cil_types.term -> loc
term
above but expects a single loc or a single
pointer value.val lemma : Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma
val vars : region -> Wp.Lang.F.Vars.t
val occurs : Wp.Lang.F.var -> region -> bool
val check_assigns : sigma ->
written:region ->
assignable:region -> Wp.Lang.F.pred