Module Wp.MemMemory

Theory

val t_malloc : Lang.F.tau

allocation tables

val t_init : Lang.F.tau Lang.extern

initialization tables

val t_mptr : Lang.F.tau Lang.extern

initialization tables

t_addr indexed array of t_attr

val t_mem : Lang.F.tau -> Lang.F.tau

t_addr indexed array of t_attr

t_addr indexed array

val f_eqmem : Lang.lfun Lang.extern
val f_memcpy : Lang.lfun Lang.extern
val sconst : Lang.F.term -> Lang.F.pred
val scinit : Lang.F.term -> Lang.F.pred
val framed : Lang.F.term -> Lang.F.pred

Unsupported Union Fields

val unsupported_union : model:string -> Frama_c_kernel.Cil_types.fieldinfo -> unit
val unsupported_bitfield : model:string -> Frama_c_kernel.Cil_types.fieldinfo -> unit