Module type MemLoader.Model

module type Model = sig .. end

Loader Model for Atomic Values


module Chunk: Sigs.Chunk 
module Sigma: Sigma  with type chunk = Chunk.t
val name : string
type loc 
val sizeof : Ctypes.c_object -> int
val field : loc -> Cil_types.fieldinfo -> loc
val shift : loc -> Ctypes.c_object -> Lang.F.term -> loc

Conversion among loc, t_pointer terms and t_addr terms

val to_addr : loc -> Lang.F.term
val to_region_pointer : loc -> int * Lang.F.term
val of_region_pointer : int -> Ctypes.c_object -> Lang.F.term -> loc
val value_footprint : Ctypes.c_object -> loc -> Sigma.domain
val init_footprint : Ctypes.c_object -> loc -> Sigma.domain
val frames : Ctypes.c_object -> loc -> Chunk.t -> Sigs.frame list
val last : Sigma.t ->
Ctypes.c_object -> loc -> Lang.F.term
val havoc : Ctypes.c_object ->
loc ->
length:Lang.F.term ->
Chunk.t -> fresh:Lang.F.term -> current:Lang.F.term -> Lang.F.term
val eqmem : Ctypes.c_object ->
loc -> Chunk.t -> Lang.F.term -> Lang.F.term -> Lang.F.pred
val eqmem_forall : Ctypes.c_object ->
loc ->
Chunk.t ->
Lang.F.term -> Lang.F.term -> Lang.F.var list * Lang.F.pred * Lang.F.pred
val load_int : Sigma.t -> Ctypes.c_int -> loc -> Lang.F.term
val load_float : Sigma.t ->
Ctypes.c_float -> loc -> Lang.F.term
val load_pointer : Sigma.t ->
Cil_types.typ -> loc -> loc
val store_int : Sigma.t ->
Ctypes.c_int -> loc -> Lang.F.term -> Chunk.t * Lang.F.term
val store_float : Sigma.t ->
Ctypes.c_float -> loc -> Lang.F.term -> Chunk.t * Lang.F.term
val store_pointer : Sigma.t ->
Cil_types.typ -> loc -> Lang.F.term -> Chunk.t * Lang.F.term
val is_init_atom : Sigma.t -> loc -> Lang.F.term
val is_init_range : Sigma.t ->
Ctypes.c_object -> loc -> Lang.F.term -> Lang.F.pred
val set_init_atom : Sigma.t ->
loc -> Lang.F.term -> Chunk.t * Lang.F.term
val set_init : Ctypes.c_object ->
loc ->
length:Lang.F.term -> Chunk.t -> current:Lang.F.term -> Lang.F.term
val monotonic_init : Sigma.t -> Sigma.t -> Lang.F.pred