Addresses (frama-c.Frama_c_kernel

Invariants of both exported modules:

Bytes is intended to represent sets of pointer values:

possible offsets of each base are expressed in bytes.
absolute addresses are represented as integers bound to Base.base.Null, allowing the same representation to be used for both integer values and absolute addresses.

Bits is intended to represent sets of lvalue addresses:

possible offsets of each base are expressed in bits, allowing it to represent the address of a bitfield.
valid absolute addresses are represented as offsets of Absolute bases, so that reads from and writes to these bases are interpreted correctly. Absolute addresses outside all valid absolute ranges are represented as integers bound to Base.base.Null.

Conversion functions Bits.of_bytes and Bits.to_bytes convert integer offsets and absolute addresses to enforce these invariants.

module Bytes : sig ... end

Association between bases and offsets in byte. Absolute addresses are represented as integers bound to Base.base.Null.

module Bits : sig ... end

Association between bases and offsets in bits. Valid absolute addresses are represented as offsets bound to Absolute bases. Absolute addresses outside all valid absolute ranges are represented as integers bound to Base.base.Null.