Module MemBytes.Model

module Chunk = Chunk
module Sigma = Sigma
val name : string
type nonrec loc = loc
val to_addr : 'a -> 'b
val to_region_pointer : 'a -> int * 'b
val of_region_pointer : 'a -> 'b -> 'c -> 'd
val value_footprint : 'a -> 'b -> Sigma.Chunk.Set.t
val init_footprint : 'a -> 'b -> Sigma.Chunk.Set.t
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 load_pointer : Sigma.t -> 'a -> Lang.F.term -> 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 set_init : Ctypes.c_object -> Lang.F.term -> length:Lang.F.term -> 'a -> current:Lang.F.term -> Lang.F.term