Module MemBytes.LOADERSource

Sourceval name : string
Sourcetype loc = loc
Sourceval pretty : Format.formatter -> loc -> unit

Conversion among loc, t_pointer terms and t_addr terms

Sourceval to_region_pointer : loc -> int * Lang.F.term
Sourceval of_region_pointer : int -> Ctypes.c_object -> Lang.F.term -> loc
Sourceval value_footprint : Ctypes.c_object -> loc -> Sigma.domain
Sourceval init_footprint : Ctypes.c_object -> loc -> Sigma.domain
Sourceval fresh : loc -> Lang.F.var list * loc
Sourceval separated : loc -> Lang.F.term -> loc -> Lang.F.term -> Lang.F.pred
Sourceval load_init_atom : Sigma.sigma -> Ctypes.c_object -> loc -> Lang.F.term