package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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.
module Domain : sig ... end