sig
module M : Model
type loc = M.loc
type nonrec value = M.loc Wp.Sigs.value
type nonrec logic = M.loc Wp.Sigs.logic
type nonrec region = M.loc Wp.Sigs.region
type nonrec result = M.loc Wp.Sigs.result
type sigma = M.Sigma.t
type frame
val pp_frame :
Stdlib.Format.formatter -> Wp.Sigs.LogicSemantics.frame -> unit
val get_frame : unit -> Wp.Sigs.LogicSemantics.frame
val in_frame : Wp.Sigs.LogicSemantics.frame -> ('a -> 'b) -> 'a -> 'b
val mem_at_frame :
Wp.Sigs.LogicSemantics.frame ->
Wp.Clabels.c_label -> Wp.Sigs.LogicSemantics.sigma
val set_at_frame :
Wp.Sigs.LogicSemantics.frame ->
Wp.Clabels.c_label -> Wp.Sigs.LogicSemantics.sigma -> unit
val has_at_frame :
Wp.Sigs.LogicSemantics.frame -> Wp.Clabels.c_label -> bool
val mem_frame : Wp.Clabels.c_label -> Wp.Sigs.LogicSemantics.sigma
val mk_frame :
?kf:Cil_types.kernel_function ->
?result:Wp.Sigs.LogicSemantics.result ->
?status:Wp.Lang.F.var ->
?formals:Wp.Sigs.LogicSemantics.value Cil_datatype.Varinfo.Map.t ->
?labels:Wp.Sigs.LogicSemantics.sigma Wp.Clabels.LabelMap.t ->
?descr:string -> unit -> Wp.Sigs.LogicSemantics.frame
val local : descr:string -> Wp.Sigs.LogicSemantics.frame
val frame : Cil_types.kernel_function -> Wp.Sigs.LogicSemantics.frame
type call
val call :
?result:M.loc ->
Cil_types.kernel_function ->
Wp.Sigs.LogicSemantics.value list -> Wp.Sigs.LogicSemantics.call
val call_pre :
Wp.Sigs.LogicSemantics.sigma ->
Wp.Sigs.LogicSemantics.call ->
Wp.Sigs.LogicSemantics.sigma -> Wp.Sigs.LogicSemantics.frame
val call_post :
Wp.Sigs.LogicSemantics.sigma ->
Wp.Sigs.LogicSemantics.call ->
Wp.Sigs.LogicSemantics.sigma Wp.Sigs.sequence ->
Wp.Sigs.LogicSemantics.frame
val return : unit -> Cil_types.typ
val result : unit -> Wp.Sigs.LogicSemantics.result
val status : unit -> Wp.Lang.F.var
val guards : Wp.Sigs.LogicSemantics.frame -> Wp.Lang.F.pred list
type env
val mk_env :
?here:Wp.Sigs.LogicSemantics.sigma ->
?lvars:Cil_types.logic_var list -> unit -> Wp.Sigs.LogicSemantics.env
val current : Wp.Sigs.LogicSemantics.env -> Wp.Sigs.LogicSemantics.sigma
val move_at :
Wp.Sigs.LogicSemantics.env ->
Wp.Sigs.LogicSemantics.sigma -> Wp.Sigs.LogicSemantics.env
val mem_at :
Wp.Sigs.LogicSemantics.env ->
Wp.Clabels.c_label -> Wp.Sigs.LogicSemantics.sigma
val env_at :
Wp.Sigs.LogicSemantics.env ->
Wp.Clabels.c_label -> Wp.Sigs.LogicSemantics.env
val lval :
Wp.Sigs.LogicSemantics.env ->
Cil_types.term_lval -> Cil_types.typ * M.loc
val term : Wp.Sigs.LogicSemantics.env -> Cil_types.term -> Wp.Lang.F.term
val pred :
Wp.Sigs.polarity ->
Wp.Sigs.LogicSemantics.env -> Cil_types.predicate -> Wp.Lang.F.pred
val region :
Wp.Sigs.LogicSemantics.env ->
unfold:bool -> Cil_types.term -> Wp.Sigs.LogicSemantics.region
val assigned_of_lval :
Wp.Sigs.LogicSemantics.env ->
unfold:bool -> Cil_types.lval -> Wp.Sigs.LogicSemantics.region
val assigned_of_froms :
Wp.Sigs.LogicSemantics.env ->
unfold:bool -> Cil_types.from list -> Wp.Sigs.LogicSemantics.region
val assigned_of_assigns :
Wp.Sigs.LogicSemantics.env ->
unfold:bool -> Cil_types.assigns -> Wp.Sigs.LogicSemantics.region option
val val_of_term :
Wp.Sigs.LogicSemantics.env -> Cil_types.term -> Wp.Lang.F.term
val loc_of_term :
Wp.Sigs.LogicSemantics.env ->
Cil_types.term -> Wp.Sigs.LogicSemantics.loc
val lemma : Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma
val vars : Wp.Sigs.LogicSemantics.region -> Wp.Lang.F.Vars.t
val occurs : Wp.Lang.F.var -> Wp.Sigs.LogicSemantics.region -> bool
val check_assigns :
Wp.Sigs.LogicSemantics.sigma ->
written:Wp.Sigs.LogicSemantics.region ->
assignable:Wp.Sigs.LogicSemantics.region -> Wp.Lang.F.pred
end