MemBytes.Model
module Chunk = Chunk
module Sigma = Sigma
type nonrec loc = loc
val sizeof : Ctypes.c_object -> Lang.F.term
val field : Lang.F.term -> Frama_c_kernel.Cil_types.fieldinfo -> Lang.F.term
val shift : Lang.F.term -> Ctypes.c_object -> Lang.F.term -> Lang.F.term
val value_footprint : 'a -> 'b -> Sigma.Chunk.Set.t
val init_footprint : 'a -> 'b -> Sigma.Chunk.Set.t
val frames :
Ctypes.c_object ->
Lang.F.term ->
Chunk.t ->
(string
* (Lang.F.var, Lang.lfun) Qed.Engine.ftrigger list
* Lang.F.pred list
* Lang.F.term
* Lang.F.term)
list
val last : Sigma.t -> Ctypes.c_object -> Lang.F.term -> Lang.F.term
val havoc :
Ctypes.c_object ->
Lang.F.term ->
length:Lang.F.term ->
Chunk.t ->
fresh:Lang.F.term ->
current:Lang.F.term ->
Lang.F.term
val eqmem :
Ctypes.c_object ->
Lang.F.term ->
'a ->
Lang.F.term ->
Lang.F.term ->
Lang.F.pred
val eqmem_forall :
Ctypes.c_object ->
Lang.F.term ->
'a ->
Lang.F.term ->
Lang.F.term ->
Lang.F.var list * Lang.F.pred * Lang.F.pred
val load_int : Sigma.t -> Ctypes.c_int -> Lang.F.term -> Lang.F.term
val load_float : Sigma.t -> CODEC_FLOAT.key -> Lang.F.term -> Lang.F.term
val load_pointer : Sigma.t -> 'a -> Lang.F.term -> Lang.F.term
val store_int :
Sigma.t ->
Ctypes.c_int ->
Lang.F.term ->
Lang.F.term ->
Chunk.t * Lang.F.term
val store_float :
Sigma.t ->
Ctypes.c_float ->
Lang.F.term ->
Lang.F.term ->
Chunk.t * Lang.F.term
val store_pointer :
Sigma.t ->
'a ->
Lang.F.term ->
Lang.F.term ->
Chunk.t * Lang.F.term
val is_init_atom : Sigma.t -> Ctypes.c_object -> Lang.F.term -> Lang.F.term
val is_init_range :
Sigma.t ->
Ctypes.c_object ->
Lang.F.term ->
Lang.F.term ->
Lang.F.pred
val set_init_atom :
Sigma.t ->
Ctypes.c_object ->
Lang.F.term ->
Lang.F.term ->
Chunk.t * Lang.F.term
val set_init :
Ctypes.c_object ->
Lang.F.term ->
length:Lang.F.term ->
'a ->
current:Lang.F.term ->
Lang.F.term