Functor Wp.LogicSemantics.Make

module Make: 
functor (M : Wp.Memory.Model) -> sig .. end
Parameters:
M : Wp.Memory.Model

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