Frama-C:
Plug-ins:
Libraries:

Frama-C API - 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_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

Frame Conditions

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

Unsupported Union Fields

val unsupported_union : Frama_c_kernel.Cil_types.fieldinfo -> unit