Exponenta Banner

Respect types in global variables (-respect-types-in-globals)

Не приводите глобальные переменные к указателям

Описание

Эта опция влияет только на анализ Code Prover.

Укажите, что глобальные переменные, первоначально не объявленные как указатели, не будут приводиться к указателям позже.

Задать опцию

Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция доступна на узле Verification Assumptions.

Командная строка и файл опций: Используйте опцию -respect-types-in-globals. См. «Информация о командной строке».

Зачем использовать эту опцию

Используйте эту опцию, чтобы идентифицировать и запретить смещения от неуказательных глобальных переменных к указателям.

Настройки

На

Эта верификация принимает, что глобальные переменные, первоначально не объявленные как указатели, не будут приведены к указателям позже.

Off (по умолчанию)

Эта верификация принимает, что глобальные переменные могут быть приведены к указателям, даже когда они не объявлены как указатели.

Совет

Если вы выберете эту опцию, количество проверок в коде может измениться. Можно использовать эту опцию и изменение результатов, чтобы идентифицировать случаи, когда вы приводите переменные, не указывающие на указатели, к указателям.

Например, в следующем примере, когда вы выбираете опцию, результаты имеют одну менее оранжевую проверку и еще одну красную проверку.

Код с отключенной опциейКод с опцией on
int global;
void main(void) {
    int local;
    global = (int)&local;
    *(int*)global = 5;
    assert(local==5);
}

В этом примере global объявлен как int переменная, но приведение к указателю. При отключенной опции Polyspace® позволяет выполнять приведение.

int global;
void main(void) {
    int local;
    global = (int)&local;
    *(int*)global = 5;
    assert(local==5);
}

В этом примере global объявлен как int переменная, но приведение к указателю. При включенной опции Polyspace игнорирует приведение. Поэтому он игнорирует инициализацию local через указатель (int*)global и создает ошибку красного Non-initialized local variable при local считывается.

Информация о командной строке

Параметр: -respect-types-in-globals
По умолчанию: Off
Пример (Code Prover): Polyspace Code Prover -sources file_name -respect-types-in-globals
Пример (Код Prover Server): Полипространство -code-prover-server -sources file_name -respect-types-in-globals

См. также

|

Темы

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

Поддержка