Frama-C API - Addresses

Represent a set of addresses by associating bases with integer offsets.

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.