Make.Mval pretty : Format.formatter -> loc -> unitval sizeof : Ctypes.c_object -> Lang.F.termval field : loc -> Frama_c_kernel.Cil_types.fieldinfo -> locval shift : loc -> Ctypes.c_object -> Lang.F.term -> locConversion among loc, t_pointer terms and t_addr terms
val to_region_pointer : loc -> int * Lang.F.termval of_region_pointer : int -> Ctypes.c_object -> Lang.F.term -> locval value_footprint : Ctypes.c_object -> loc -> Sigma.domainval init_footprint : Ctypes.c_object -> loc -> Sigma.domainval last : Sigma.sigma -> Ctypes.c_object -> loc -> Lang.F.termval fresh : loc -> Lang.F.var list * locval separated : loc -> Lang.F.term -> loc -> Lang.F.term -> Lang.F.predval eqmem :
Sigma.Chunk.t ->
Lang.F.term ->
Lang.F.term ->
loc ->
Lang.F.term ->
Lang.F.predval memcpy :
Sigma.Chunk.t ->
Lang.F.term ->
loc ->
Lang.F.term ->
loc ->
Lang.F.term ->
Lang.F.termval load_int : Sigma.sigma -> Ctypes.c_int -> loc -> Lang.F.termval load_float : Sigma.sigma -> Ctypes.c_float -> loc -> Lang.F.termval load_pointer : Sigma.sigma -> Frama_c_kernel.Cil_types.typ -> loc -> locval load_init_atom : Sigma.sigma -> Ctypes.c_object -> loc -> Lang.F.termval store_int :
Sigma.sigma ->
Ctypes.c_int ->
loc ->
Lang.F.term ->
Sigma.Chunk.t * Lang.F.termval store_float :
Sigma.sigma ->
Ctypes.c_float ->
loc ->
Lang.F.term ->
Sigma.Chunk.t * Lang.F.termval store_pointer :
Sigma.sigma ->
Frama_c_kernel.Cil_types.typ ->
loc ->
Lang.F.term ->
Sigma.Chunk.t * Lang.F.termval store_init_atom :
Sigma.sigma ->
Ctypes.c_object ->
loc ->
Lang.F.term ->
Sigma.Chunk.t * Lang.F.term