Module MemTyped

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 = 
| NoCast
| Fits
| Unsafe
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
val footprint : Ctypes.c_object -> Heap.Set.t
val footprint_comp : 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
val name : string
type key = MemTyped.LITERAL.t 
type data = Lang.F.term 
val linked : string -> Lang.F.term -> Cstring.cst -> unit
val region : string -> Lang.F.term -> Cstring.cst -> unit
val sconst : string -> Lang.F.term -> Cstring.cst -> unit
val compile : int * Cstring.cst -> Lang.F.term
end)
module BASE: Model.Generator(Cil_datatype.Varinfo)(sig
val name : string
type key = Cil_types.varinfo 
type data = Lang.F.term 
val region : string -> Cil_types.varinfo -> Lang.F.term -> unit
val linked : string -> Cil_types.varinfo -> Lang.F.term -> unit
val generate : Cil_types.varinfo -> Lang.F.term
val compile : Cil_types.varinfo -> Lang.F.term
end)
module MONOTONIC: sig .. end
module COMP: Model.Generator(Cil_datatype.Compinfo)(sig
val name : string
type key = Cil_types.compinfo 
type data = Lang.lfun * MemTyped.chunk list 
val generate : Cil_types.compinfo -> Lang.lfun * MemTyped.Heap.Set.elt list
val compile : Cil_types.compinfo -> Lang.lfun * MemTyped.Heap.Set.elt list
end)
module ARRAY: Model.Generator(Matrix.NATURAL)(sig
val name : string
type key = Matrix.matrix 
type data = Lang.lfun * MemTyped.chunk list 
val generate : Ctypes.c_object * Matrix.dim list -> Lang.lfun * MemTyped.Heap.Set.elt list
val compile : Ctypes.c_object * Matrix.dim list -> Lang.lfun * MemTyped.Heap.Set.elt list
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 = 
| ALLOC
| FREE
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