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