Документация

Отображает список переменных и функций в проекте, для которых можно задать области значений данных.

В этом столбце отображаются три элементов меню с возможностью расширения:

Отображает информацию о переменной или функции.

Для примера статические переменные отображения static. Незакрытые функции отображают unused.

Применяется только для пользовательских функций.

Определяет, вызывает ли основной генератор функцию:

Определяет, как программа присваивает область значений переменной:

Пользовательские функции поддерживают только INIT режим.

Функции заглушки поддерживают только PERMANENT режим.

Для верификаций на C глобальные указатели поддерживают MAIN GENERATOR, IGNORE, или INIT режим.

Задает минимальное и максимальное значения для переменной.

Можно использовать ключевые слова min и max для обозначения минимального и максимального значений типа переменной. Для примера, для типа long, min и max соответствуют -2 ^ 31 и 2 ^ 31-1 соответственно.

Можно также использовать шестнадцатеричные значения. Для примера: 0x12..0x100

Для enum переменные, вы не можете задать области значений непосредственно с помощью констант перечислителя. Вместо этого используйте значения, представленные константами.

Для enum переменные, можно также использовать ключевые слова enum_min и enum_max чтобы обозначить минимальное и максимальное значения, которые может взять переменная. Для примера, для enum переменная заданного ниже типа, enum_min 0 и enum_max 5:

enum week{ sunday, monday=0, tuesday, wednesday, thursday, friday, saturday};

Применимо только к указателям. Включено только при задании Init Mode: INIT.

Указывает, должен ли указатель иметь значение NULL:

Применимо только к указателям. Включено только при задании Init Mode: INIT.

Определяет, как выделяется заостренный объект:

В сложение для аргументов указателя на упорные функции доступны две другие опции:

Для упрямых функций опции SINGLE и MULTI означает вероятную инициализацию вместо определенной инициализации.

Применимо только к указателям.

Задает, на сколько объектов указывает указатель (заостренный объект рассматривается как массив).

Параметр Init Allocated определяет, сколько выделенных объектов фактически инициализировано. Например, рассмотрим этот код:

void func(int *ptr) {
    assert(ptr[0]==1);
    assert(ptr[1]==1);
}

оба утверждения зеленого цвета. Однако, если вы задаете эти ограничения:

второе утверждение оранжевого цвета. Только первый объект, который ptr указывает на инициализированное значение 1. Объекты за пределами первого могут быть потенциально полной областью значений.