Module MemTyped

module MemTyped: sig .. end

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_mk_addr : 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_mk_addr : Lang.F.term -> 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_shift : Lang.F.Fun.t -> Lang.F.term -> Lang.F.term -> Lang.F.term
type registered_shift = 
| RS_Field of Lang.F.term
| RS_Shift of Lang.F.Z.t
module RegisterShift: Model.Static(sig
type key = Lang.lfun 
type data = MemTyped.registered_shift 
val name : string
include Lang.Fun
end)
val phi_base : Lang.F.term -> Lang.F.term
val phi_offset : 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 r_included : range -> range -> Lang.F.pred
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 cluster_globals : unit -> Definitions.cluster
val cluster_memory : unit -> Definitions.cluster
module ShiftField: Model.Generator(Cil_datatype.Fieldinfo)(sig
val name : string
type key = Cil_types.fieldinfo 
type data = Lang.lfun 
val generate : Cil_datatype.Fieldinfo.t -> Lang.lfun
val compile : Cil_datatype.Fieldinfo.t -> Lang.lfun
end)
module Shift: Model.Generator(sig
type t = Ctypes.c_object 
val pretty : Format.formatter -> Ctypes.C_object.t -> unit
val compare : Ctypes.c_object -> Ctypes.c_object -> int
end)(sig
val name : string
type key = Ctypes.c_object 
type data = Lang.lfun 
val c_object_id : Ctypes.c_object -> string
val c_object_id : Ctypes.c_object -> string
val generate : Ctypes.c_object -> Lang.lfun
val compile : Ctypes.c_object -> Lang.lfun
end)
val field : Lang.F.term -> ShiftField.key -> Lang.F.term
val shift : Lang.F.term -> Shift.key -> Lang.F.term -> Lang.F.term
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 ->
Shift.key ->
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
val global : 'a -> Lang.F.term -> Lang.F.pred
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