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