module MTypedRef: MemVar.Make
(
VarRef2
)
(
MemTyped
)
val datatype : string
val configure : Model.tuning
type
chunk =
val is_framed_var : Cil_types.varinfo -> bool
module VAR: sig
.. end
module VALLOC: sig
.. end
module Chunk: sig
.. end
module HEAP: Qed.Collection.Make
(
VAR
)
module TALLOC: Qed.Collection.Make
(
VALLOC
)
module SIGMA: Sigma.Make
(
VAR
)
(
HEAP
)
module ALLOC: Sigma.Make
(
VALLOC
)
(
TALLOC
)
module Heap: Qed.Collection.Make
(
Chunk
)
type
sigma = {
|
mem : M.Sigma.t ; |
|
vars : SIGMA.t ; |
|
alloc : ALLOC.t ; |
}
module Sigma: sig
.. end
val get_var : sigma -> SIGMA.chunk -> Lang.F.var
val get_term : sigma -> SIGMA.chunk -> Lang.F.term
type
loc =
type
ofs =
type
segment = loc Memory.rloc
val pp_ofs : Format.formatter -> ofs list -> unit
val pretty : Format.formatter -> loc -> unit
val ofs_vars : Lang.F.Vars.t -> ofs list -> Lang.F.Vars.t
val vars : loc -> Lang.F.Vars.t
val ofs_occurs : Lang.F.Vars.elt -> ofs list -> bool
val occurs : Lang.F.var -> loc -> bool
val null : loc
val literal : eid:int -> Cstring.cst -> loc
val cvar : Cil_types.varinfo -> loc
val mloc : Cil_types.varinfo -> ofs list -> M.loc
val mloc_of_loc : loc -> M.loc
val pointer_loc : Lang.F.term -> loc
val pointer_val : loc -> Lang.F.term
val field : loc -> Cil_types.fieldinfo -> loc
val index : ofs list ->
Ctypes.c_object -> Lang.F.term -> ofs list
val shift : loc -> Ctypes.c_object -> Lang.F.term -> loc
val base_addr : loc -> loc
val block_length : sigma -> Ctypes.c_object -> loc -> Lang.F.term
val cast : Ctypes.c_object Memory.sequence -> loc -> loc
val loc_of_int : Ctypes.c_object -> Lang.F.term -> loc
val int_of_loc : Ctypes.c_int -> loc -> Lang.F.term
val access : Lang.F.term -> ofs list -> Lang.F.term
val update : Lang.F.term -> ofs list -> Lang.F.term -> Lang.F.term
val mload : sigma -> Ctypes.c_object -> M.loc -> loc Memory.value
val load : sigma ->
Ctypes.c_object -> loc -> loc Memory.value
val mstored : sigma Memory.sequence ->
Ctypes.c_object -> M.loc -> Lang.F.term -> Lang.F.pred list
val stored : sigma Memory.sequence ->
Ctypes.c_object -> loc -> Lang.F.term -> Lang.F.pred list
val copied : sigma Memory.sequence ->
Ctypes.c_object -> loc -> loc -> Lang.F.pred list
val is_null : loc -> Lang.F.pred
val offset : ofs list -> Lang.F.term
val loc_diff : Ctypes.c_object -> loc -> loc -> Lang.F.term
val loc_compare : (M.loc -> M.loc -> Lang.F.pred) ->
(Lang.F.term -> Lang.F.term -> Lang.F.pred) ->
Lang.F.pred -> loc -> loc -> Lang.F.pred
val loc_eq : loc -> loc -> Lang.F.pred
val loc_lt : loc -> loc -> Lang.F.pred
val loc_leq : loc -> loc -> Lang.F.pred
val loc_neq : loc -> loc -> Lang.F.pred
val size_of_array_type : Cil_types.typ -> Lang.F.term option
val first_index : Lang.F.term option
val range_offset : Cil_types.typ -> Lang.F.term -> Lang.F.pred
val valid_offset : Cil_types.typ -> ofs list -> Lang.F.pred
val valid_offsetrange : Cil_types.typ ->
ofs list ->
Lang.F.term option -> Lang.F.term option -> Lang.F.pred
val valid_base : sigma -> ALLOC.chunk -> Lang.F.pred
val valid_path : sigma ->
ALLOC.chunk ->
Cil_types.typ -> ofs list -> Lang.F.pred
val valid_pathrange : sigma ->
ALLOC.chunk ->
Cil_types.typ ->
ofs list ->
Lang.F.term option -> Lang.F.term option -> Lang.F.pred
val valid_loc : sigma ->
Memory.acs -> Ctypes.c_object -> loc -> Lang.F.pred
val valid_range : sigma ->
Memory.acs ->
loc ->
Ctypes.c_object -> Lang.F.term option -> Lang.F.term option -> Lang.F.pred
val valid_array : sigma ->
Memory.acs -> loc -> Ctypes.c_object -> int -> Lang.F.pred
val valid : sigma -> Memory.acs -> loc Memory.rloc -> Lang.F.pred
val is_mem : Cil_types.varinfo -> bool
val is_ref : Cil_types.varinfo -> bool
val alloc_var : ALLOC.t ->
TALLOC.Set.t -> Lang.F.term -> Lang.F.pred list
val allocates : ALLOC.t ->
TALLOC.Set.elt list ->
bool -> ALLOC.t * Lang.F.pred list
val scope_vars : ALLOC.t ->
Mcfg.scope ->
TALLOC.Set.elt list -> ALLOC.t * Lang.F.pred list
val scope : sigma ->
Mcfg.scope ->
TALLOC.Set.elt list -> sigma * Lang.F.pred list
type
seq =
type
delta =
val dofs : ofs -> delta
val delta : ofs list -> delta list
val range : ofs list ->
Ctypes.c_object ->
Lang.F.term option -> Lang.F.term option -> delta list
val dsize : int -> delta
val rsize : ofs list -> int -> delta list
val locseg : loc Memory.rloc -> seq
val included_delta : delta list -> delta list -> Lang.F.pred
val included : loc Memory.rloc -> loc Memory.rloc -> Lang.F.pred
val separated_delta : delta list -> delta list -> Lang.F.pred
val separated : loc Memory.rloc -> loc Memory.rloc -> Lang.F.pred
val sloc_descr : loc Memory.sloc ->
Lang.F.var list * loc * Lang.F.pred
val floc_path : loc -> Cil_types.varinfo * ofs list
val assigned_path : Lang.F.pred list ->
Lang.F.var list ->
Lang.F.var list ->
Lang.F.term -> Lang.F.term -> ofs list -> Lang.F.pred list
val assigned : sigma Memory.sequence ->
Ctypes.c_object -> loc Memory.sloc -> Lang.F.pred list
val domain : Ctypes.c_object -> loc -> Heap.Set.t