package frama-c

  1. Overview
  2. Docs

Module Wp.MemMemorySource

Theory

Sourceval t_addr : Lang.F.tau
Sourceval t_malloc : Lang.F.tau

allocation tables

Sourceval t_init : Lang.F.tau

initialization tables

t_addr indexed array

Sourceval a_null : Lang.F.term

Null address. Same as a_addr 0 0

Sourceval a_global : Lang.F.term -> Lang.F.term

Zero-offset base. Same as a_addr base 0

Constructor for { base ; offset }

Shift: a_shift a k adds k to a.offset

Returns the base

Sourceval a_offset : Lang.F.term -> Lang.F.term

Returns the offset

Sourceval a_base_offset : Lang.F.term -> Lang.F.term -> Lang.F.term

Returns the offset in bytes from the logic offset (which is a memory cell index, actually)

Sourceval f_null : Lang.lfun
Sourceval f_base : Lang.lfun
Sourceval f_global : Lang.lfun
Sourceval f_shift : Lang.lfun
Sourceval f_offset : Lang.lfun
Sourceval f_havoc : Lang.lfun
Sourceval f_set_init : Lang.lfun
Sourceval f_region : Lang.lfun
Sourceval f_addr_of_int : Lang.lfun

Physical address

Sourceval f_int_of_addr : Lang.lfun

Physical address

Sourceval p_addr_lt : Lang.lfun
Sourceval p_addr_le : Lang.lfun
Sourceval p_linked : Lang.lfun
Sourceval p_framed : Lang.lfun
Sourceval p_sconst : Lang.lfun
Sourceval p_cinits : Lang.lfun
Sourceval p_is_init_r : Lang.lfun
Sourceval p_separated : Lang.lfun
Sourceval p_included : Lang.lfun
Sourceval p_valid_rd : Lang.lfun
Sourceval p_valid_rw : Lang.lfun
Sourceval p_valid_obj : Lang.lfun
Sourceval p_invalid : Lang.lfun
Sourceval p_eqmem : Lang.lfun
Sourceval p_monotonic : Lang.lfun

Addr Producer Registration

Register simplifiers for functions producing addr terms:

  • ~base es is the simplifier for (f es).base
  • ~offset es is the simplifier for (f es).offset
  • ~linear:true register simplifier f(f(p,i),k)=f(p,i+j) on f
  • ~equal a b is the set_eq_builtin for f

The equality builtin is wrapped inside a default builtin that compares f es by computing base and offset.

Sourceval register : ?base:(Lang.F.term list -> Lang.F.term) -> ?offset:(Lang.F.term list -> Lang.F.term) -> ?equal:(Lang.F.term -> Lang.F.term -> Lang.F.pred) -> ?linear:bool -> Lang.lfun -> unit

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.

Sourceval frames : addr:Lang.F.term -> offset:Lang.F.term -> sizeof:Lang.F.term -> ?basename:string -> Lang.F.tau -> Sigs.frame list

Range of Address

Sourceval separated : shift:('a -> Ctypes.c_object -> Lang.F.term -> 'a) -> addrof:('a -> Lang.F.term) -> sizeof:(Ctypes.c_object -> Lang.F.term) -> 'a Sigs.rloc -> 'a Sigs.rloc -> Lang.F.pred
Sourceval included : shift:('a -> Ctypes.c_object -> Lang.F.term -> 'a) -> addrof:('a -> Lang.F.term) -> sizeof:(Ctypes.c_object -> Lang.F.term) -> 'a Sigs.rloc -> 'a Sigs.rloc -> Lang.F.pred

Unsupported Union Fields

Sourceval unsupported_union : Frama_c_kernel.Cil_types.fieldinfo -> unit