Module `MemBytes.LOADER`Source

Sourceval name : string

Sourcetype loc = loc

Sourceval pretty : Stdlib.Format.formatter -> loc -> unit

Sourceval sizeof : Ctypes.c_object -> Lang.F.term

Sourceval field : loc -> Frama_c_kernel.Cil_types.fieldinfo -> loc

Sourceval shift : loc -> Ctypes.c_object -> Lang.F.term -> loc

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 last : Sigma.sigma -> Ctypes.c_object -> loc -> Lang.F.term

Sourceval fresh : loc -> Lang.F.var list * loc

Sourceval separated : loc -> Lang.F.term -> loc -> Lang.F.term -> Lang.F.pred

val eqmem : 
  Sigma.Chunk.t ->
  Lang.F.term ->
  Lang.F.term ->
  loc ->
  Lang.F.term ->
  Lang.F.pred

val memcpy : 
  Sigma.Chunk.t ->
  Lang.F.term ->
  loc ->
  Lang.F.term ->
  loc ->
  Lang.F.term ->
  Lang.F.term

Sourceval load_int : Sigma.sigma -> Ctypes.c_int -> loc -> Lang.F.term

Sourceval load_float : Sigma.sigma -> Ctypes.c_float -> loc -> Lang.F.term

Sourceval load_pointer : Sigma.sigma -> Frama_c_kernel.Cil_types.typ -> loc -> loc

Sourceval load_init_atom : Sigma.sigma -> Ctypes.c_object -> loc -> Lang.F.term

val store_int : 
  Sigma.sigma ->
  Ctypes.c_int ->
  loc ->
  Lang.F.term ->
  Sigma.Chunk.t * Lang.F.term

val store_float : 
  Sigma.sigma ->
  Ctypes.c_float ->
  loc ->
  Lang.F.term ->
  Sigma.Chunk.t * Lang.F.term

val store_pointer : 
  Sigma.sigma ->
  Frama_c_kernel.Cil_types.typ ->
  loc ->
  Lang.F.term ->
  Sigma.Chunk.t * Lang.F.term

val store_init_atom : 
  Sigma.sigma ->
  Ctypes.c_object ->
  loc ->
  Lang.F.term ->
  Sigma.Chunk.t * Lang.F.term

Install