Wp.MemMemory
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_havoc : Lang.lfun
val f_set_init : Lang.lfun
val p_is_init_r : Lang.lfun
val p_eqmem : Lang.lfun
val p_monotonic : Lang.lfun
val cinits : Lang.F.term -> Lang.F.pred
val sconst : Lang.F.term -> Lang.F.pred
val framed : Lang.F.term -> Lang.F.pred
frames ~addr
are frame conditions for reading a value at address addr
from a chunk of memory. The value read at addr
have length offset
, while individual element in memory chunk have type tau
and offset length sizeof
.
Memory variables use ~basename
or "mem"
by default.
val frames :
addr:Lang.F.term ->
offset:Lang.F.term ->
sizeof:Lang.F.term ->
?basename:string ->
Lang.F.tau ->
Sigs.frame list
val unsupported_union : Frama_c_kernel.Cil_types.fieldinfo -> unit