Module Wp.MemMemory

Theory

val t_malloc : Lang.F.tau

allocation tables

val t_init : Lang.F.tau

initialization tables

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

t_addr indexed array

val f_eqmem : Lang.lfun
val f_memcpy : Lang.lfun
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