module MemTyped: sig
.. end
Since its a generated it is the unique name given
module L: Qed.Logic
val datatype : string
val library : string
val a_addr : Lang.F.term -> Lang.F.term -> Lang.F.term
val t_addr : ('a, Lang.adt) L.datatype
val f_base : Lang.lfun
val f_offset : Lang.lfun
val f_shift : Lang.lfun
val f_global : Lang.lfun
val f_null : Lang.lfun
val p_valid_rd : Lang.lfun
val p_valid_rw : Lang.lfun
val p_separated : Lang.lfun
val p_included : Lang.lfun
val p_eqmem : Lang.lfun
val p_havoc : Lang.lfun
val f_region : Lang.lfun
val p_framed : Lang.lfun
val p_linked : Lang.lfun
val p_sconst : Lang.lfun
val a_lt : Lang.lfun
val a_leq : Lang.lfun
val a_cast : Lang.lfun
val a_hardware : Lang.lfun
val a_null : Lang.F.term
val a_base : Lang.F.term -> Lang.F.term
val a_offset : Lang.F.term -> Lang.F.term
val a_global : Lang.F.term -> Lang.F.term
val a_shift : Lang.F.term -> Lang.F.term -> Lang.F.term
val a_addr : Lang.F.term -> Lang.F.term -> Lang.F.term
val phi_base : Lang.F.term -> Lang.F.term
val phi_offset : Lang.F.term -> Lang.F.term
val phi_shift : Lang.F.term -> Lang.F.term -> Lang.F.term
val eq_shift : Lang.F.term -> Lang.F.term -> Lang.F.pred
val r_separated : Lang.F.term list -> Lang.F.term
val configure : unit -> unit
type
pointer =
val pointer : pointer Context.value
type
chunk =
| |
M_int |
| |
M_char |
| |
M_float |
| |
M_pointer |
| |
T_alloc |
module Chunk: sig
.. end
module Heap: Qed.Collection.Make
(
Chunk
)
module Sigma: Sigma.Make
(
Chunk
)
(
Heap
)
type
loc = Lang.F.term
val m_int : Ctypes.c_int -> chunk
: Ctypes.c_object -> Heap.Set.t
: Cil_types.compinfo -> Heap.Set.t
val signature : Heap.Set.t ->
Lang.F.var list * Heap.Set.elt list * Sigma.t
val memories : Sigma.t -> Sigma.chunk list -> Lang.F.term list
val size_of_object : Ctypes.c_object -> int
val size_of_typ : Cil_types.typ -> int
val size_of_field : Cil_types.fieldinfo -> int
val size_of_comp : Cil_types.compinfo -> int
val offset_of_field : Cil_datatype.Fieldinfo.t -> int
type
sigma = Sigma.t
type
segment = loc Memory.rloc
val pretty : Format.formatter -> Lang.F.term -> unit
val vars : Lang.F.term -> Lang.F.Vars.t
val occurs : Lang.F.var -> Lang.F.term -> bool
val loadrec : (Sigma.t -> Ctypes.c_object -> Lang.F.term -> Lang.F.term)
Pervasives.ref
val field : Lang.F.term -> Cil_datatype.Fieldinfo.t -> Lang.F.term
val shift : Lang.F.term -> Ctypes.c_object -> Lang.F.term -> Lang.F.term
val cluster_globals : unit -> Definitions.cluster
val cluster_memory : unit -> Definitions.cluster
module LITERAL: sig
.. end
module STRING: Model.Generator
(
LITERAL
)
(
sig
end
)
module BASE: Model.Generator
(
Cil_datatype.Varinfo
)
(
sig
end
)
module MONOTONIC: sig
.. end
module COMP: Model.Generator
(
Cil_datatype.Compinfo
)
(
sig
end
)
module ARRAY: Model.Generator
(
Matrix.NATURAL
)
(
sig
end
)
val loadvalue : Sigma.t -> Ctypes.c_object -> Lang.F.term -> Lang.F.term
val load : Sigma.t -> Ctypes.c_object -> Lang.F.term -> 'a Memory.value
val null : Lang.F.term
val literal : eid:int -> Cstring.cst -> Lang.F.term
val cvar : BASE.key -> Lang.F.term
val pointer_loc : 'a -> 'a
val pointer_val : 'a -> 'a
val get_alloc : Sigma.t -> Lang.F.term -> Lang.F.term
val get_last : Sigma.t -> Lang.F.term -> Lang.F.term
val base_addr : Lang.F.term -> Lang.F.term
val block_length : Sigma.t -> Ctypes.c_object -> Lang.F.term -> Lang.F.term
module Layout: sig
.. end
val pp_mismatch : Format.formatter -> Ctypes.c_object Memory.sequence -> unit
val cast : Ctypes.c_object Memory.sequence -> Lang.F.term -> Lang.F.term
val loc_of_int : 'a -> Lang.F.term -> Lang.F.term
val int_of_loc : 'a -> Lang.F.term -> Lang.F.term
val domain : Ctypes.c_object -> 'a -> Heap.Set.t
val updated : Sigma.t Memory.sequence ->
Sigma.chunk -> Lang.F.term -> Lang.F.term -> Lang.F.pred list
val havoc_range : Sigma.t Memory.sequence ->
Ctypes.c_object -> Lang.F.term -> Lang.F.term -> Lang.F.pred list
val havoc : Sigma.t Memory.sequence ->
Ctypes.c_object -> Lang.F.term -> Lang.F.pred list
val eqmem : Sigma.t Memory.sequence ->
Ctypes.c_object -> Lang.F.term -> Lang.F.pred list
val stored : Sigma.t Memory.sequence ->
Ctypes.c_object -> Lang.F.term -> Lang.F.term -> Lang.F.pred list
val copied : Sigma.t Memory.sequence ->
Ctypes.c_object -> Lang.F.term -> Lang.F.term -> Lang.F.pred list
val assigned_loc : Sigma.t Memory.sequence ->
Ctypes.c_object -> Lang.F.term -> Lang.F.pred list
val equal_loc : Sigma.t Memory.sequence ->
Ctypes.c_object -> Lang.F.term -> Lang.F.pred list
val assigned_range : Sigma.t Memory.sequence ->
Ctypes.c_object ->
Lang.F.term -> Lang.F.term -> Lang.F.term -> Lang.F.pred list
val assigned : Sigma.t Memory.sequence ->
Ctypes.c_object -> Lang.F.term Memory.sloc -> Lang.F.pred list
val loc_compare : Lang.lfun ->
(Lang.F.term -> Lang.F.term -> Lang.F.pred) ->
Lang.F.term -> Lang.F.term -> Lang.F.pred
val is_null : Lang.F.term -> Lang.F.pred
val loc_eq : Lang.F.term -> Lang.F.term -> Lang.F.pred
val loc_neq : Lang.F.term -> Lang.F.term -> Lang.F.pred
val loc_lt : Lang.F.term -> Lang.F.term -> Lang.F.pred
val loc_leq : Lang.F.term -> Lang.F.term -> Lang.F.pred
val loc_diff : Ctypes.c_object -> Lang.F.term -> Lang.F.term -> Lang.F.term
val s_valid : Sigma.t -> Memory.acs -> Lang.F.term -> Lang.F.term -> Lang.F.pred
val access : Memory.acs -> Lang.F.term -> Lang.F.pred
val valid : Sigma.t -> Memory.acs -> Lang.F.term Memory.rloc -> Lang.F.pred
type
alloc =
val allocates : Sigma.t ->
BASE.key list ->
alloc -> Sigma.t * Lang.F.pred list
val framed : Sigma.t -> Lang.F.pred list
val scope : Sigma.t ->
Mcfg.scope -> BASE.key list -> Sigma.t * Lang.F.pred list
type
range =
| |
LOC of Lang.F.term * Lang.F.term |
| |
RANGE of Lang.F.term * Vset.set |
val range : Lang.F.term Memory.rloc -> range
val range_set : range -> Lang.F.term * Vset.set
val r_included : range -> range -> Lang.F.pred
val r_disjoint : range -> range -> Lang.F.pred
val included : Lang.F.term Memory.rloc -> Lang.F.term Memory.rloc -> Lang.F.pred
val separated : Lang.F.term Memory.rloc -> Lang.F.term Memory.rloc -> Lang.F.pred