Module Memory.Smashing

Abstraction of arrays by smashing.

This domain summarizes the initialized values of a base using single smash variable `smash(base)`.

In order to determine whether the accessed element has been initialized, the domain uses a numeric variable `uninit(base)` that tracks the offset of the first unintilialized element of memory block `base`.

The concretization of this domain is therefore:

∀ i ∈ 0, uninit(base) - 1: basei ∈ γ(smash(base))

For efficiency reason, some specific values of `uninit(base)` are directly encoded in the abstract state. More particularly, the domain uses two shortcut states:

• Init.None : used to denote that the base has not been initialized yet. This corresponds to `uninit(base) = 0`.

• Init.Full : used to denote that the base has been fully initialized. This corresponds to `uninit(base) = size(base)`.

Limitations:

• Considers only (multi-)arrays of scalars.
• Supports only sequential initialization starting from offset 0.
• memcpy-like formulas limited to numeric arrays where the destination is fully covered.