functor (M : Memory.Model) ->
sig
type loc = M.loc
type sigma = M.Sigma.t
type value = M.loc Wp.Memory.value
type logic = M.loc Wp.Memory.logic
type region = M.loc Wp.Memory.sloc list
val pp_logic : Format.formatter -> Wp.LogicSemantics.Make.logic -> unit
val pp_sloc :
Format.formatter -> Wp.LogicSemantics.Make.loc Wp.Memory.sloc -> unit
val pp_region : Format.formatter -> Wp.LogicSemantics.Make.region -> unit
type call
type frame
val pp_frame : Format.formatter -> Wp.LogicSemantics.Make.frame -> unit
val get_frame : unit -> Wp.LogicSemantics.Make.frame
val in_frame : Wp.LogicSemantics.Make.frame -> ('a -> 'b) -> 'a -> 'b
val mem_frame : Wp.Clabels.c_label -> Wp.LogicSemantics.Make.sigma
val mem_at_frame :
Wp.LogicSemantics.Make.frame ->
Wp.Clabels.c_label -> Wp.LogicSemantics.Make.sigma
val call :
Cil_types.kernel_function ->
Wp.LogicSemantics.Make.value list -> Wp.LogicSemantics.Make.call
val frame : Cil_types.kernel_function -> Wp.LogicSemantics.Make.frame
val call_pre :
Wp.LogicSemantics.Make.sigma ->
Wp.LogicSemantics.Make.call ->
Wp.LogicSemantics.Make.sigma -> Wp.LogicSemantics.Make.frame
val call_post :
Wp.LogicSemantics.Make.sigma ->
Wp.LogicSemantics.Make.call ->
Wp.LogicSemantics.Make.sigma Wp.Memory.sequence ->
Wp.LogicSemantics.Make.frame
val return : unit -> Cil_types.typ
val result : unit -> Wp.Lang.F.var
val status : unit -> Wp.Lang.F.var
val guards : Wp.LogicSemantics.Make.frame -> Wp.Lang.F.pred list
type env
val new_env : Cil_types.logic_var list -> Wp.LogicSemantics.Make.env
val move :
Wp.LogicSemantics.Make.env ->
Wp.LogicSemantics.Make.sigma -> Wp.LogicSemantics.Make.env
val sigma : Wp.LogicSemantics.Make.env -> Wp.LogicSemantics.Make.sigma
val mem_at :
Wp.LogicSemantics.Make.env ->
Wp.Clabels.c_label -> Wp.LogicSemantics.Make.sigma
val call_env : Wp.LogicSemantics.Make.sigma -> Wp.LogicSemantics.Make.env
val term : Wp.LogicSemantics.Make.env -> Cil_types.term -> Wp.Lang.F.term
val pred :
Wp.LogicSemantics.polarity ->
Wp.LogicSemantics.Make.env -> Cil_types.predicate -> Wp.Lang.F.pred
val region :
Wp.LogicSemantics.Make.env ->
Cil_types.term -> Wp.LogicSemantics.Make.region
val assigns :
Wp.LogicSemantics.Make.env ->
Cil_types.identified_term Cil_types.assigns ->
(Wp.Ctypes.c_object * Wp.LogicSemantics.Make.region) list option
val assigns_from :
Wp.LogicSemantics.Make.env ->
Cil_types.identified_term Cil_types.from list ->
(Wp.Ctypes.c_object * Wp.LogicSemantics.Make.region) list
val val_of_term :
Wp.LogicSemantics.Make.env -> Cil_types.term -> Wp.Lang.F.term
val loc_of_term :
Wp.LogicSemantics.Make.env ->
Cil_types.term -> Wp.LogicSemantics.Make.loc
val lemma : Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma
val vars : Wp.LogicSemantics.Make.region -> Wp.Lang.F.Vars.t
val occurs : Wp.Lang.F.var -> Wp.LogicSemantics.Make.region -> bool
val valid :
Wp.LogicSemantics.Make.sigma ->
Wp.Memory.acs ->
Wp.Ctypes.c_object -> Wp.LogicSemantics.Make.region -> Wp.Lang.F.pred
val included :
Wp.Ctypes.c_object ->
Wp.LogicSemantics.Make.region ->
Wp.Ctypes.c_object -> Wp.LogicSemantics.Make.region -> Wp.Lang.F.pred
val separated :
(Wp.Ctypes.c_object * Wp.LogicSemantics.Make.region) list ->
Wp.Lang.F.pred
end