Module `Wp.MemMemory`Source

Theory

Sourceval t_malloc : Lang.F.tau

allocation tables

Sourceval t_init : Lang.F.tau

initialization tables

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

t_addr indexed array

Sourceval f_havoc : Lang.lfun

Sourceval f_set_init : Lang.lfun

Sourceval p_is_init_r : Lang.lfun

Sourceval p_eqmem : Lang.lfun

Sourceval p_monotonic : Lang.lfun

Sourceval cinits : Lang.F.term -> Lang.F.pred

Sourceval sconst : Lang.F.term -> Lang.F.pred

Sourceval 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.

Source

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

Sourceval unsupported_union : Frama_c_kernel.Cil_types.fieldinfo -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/MemMemory/index.html

Module `Wp.MemMemory`Source

Theory

Frame Conditions

Unsupported Union Fields

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/MemMemory/index.html

Module Wp.MemMemorySource

Theory

Frame Conditions

Unsupported Union Fields

Module `Wp.MemMemory`Source