module Make:
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
Debug
val pp_logic : Format.formatter -> logic -> unit
val pp_sloc : Format.formatter -> loc 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 : Clabels.c_label -> sigma
val mem_at_frame : frame -> 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 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
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 -> Clabels.c_label -> sigma
val call_env : sigma -> env
val term : env -> Cil_types.term -> Lang.F.term
val pred : LogicSemantics.polarity ->
env -> Cil_types.predicate -> Lang.F.pred
val region : env -> Cil_types.term -> region
val assigns : env ->
Cil_types.assigns ->
(Ctypes.c_object * region) list option
val assigns_from : env ->
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
Regions
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