Exponenta Banner
exponenta event banner

Типы уважения в глобальных переменных (-respect-types-in-globals)

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

Описание

Этот параметр влияет только на анализ программы проверки кода.

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

Задать опцию

Пользовательский интерфейс (только для настольных ПК): в конфигурации проекта эта опция доступна в узле Проверочные допущения.

файл командной строки и параметров: Использовать параметр -respect-types-in-globals. См. раздел Сведения о командной строке.

Зачем использовать этот параметр

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

Настройки

На

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

Выкл. (по умолчанию)

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

Совет

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

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

Код с выключенной опциейКод с опцией 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 переменная, но приведенная к указателю. При включенной опции Полиспейс игнорирует отливку. Поэтому он игнорирует инициализацию local через указатель (int*)global и создает красную неинициализированную ошибку локальной переменной, когда local считывается.

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

Параметр: -respect-types-in-globals
По умолчанию: Откл.
Пример (проверка кода): polyspace-code-prover -sources file_name -respect-types-in-globals
Пример (сервер проверки кода): polyspace-code-prover-server -sources file_name -respect-types-in-globals

См. также

|

Темы

Документация по программе проверки кода Polyspace

Поддержка