Ignore default initialization of global variables (-no-def-init-glob)

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

Описание

Эта опция применяется только к Code Prover. Это не влияет на анализ Bug Finder.

Задайте, что Polyspace® не следует рассматривать глобальные и статические переменные как инициализированные, если они явным образом не инициализированы в коде.

Задать опцию

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

Командная строка и файл опций: Используйте опцию -no-def-init-glob. См. «Информация о командной строке».

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

Стандарт C99 задает, что глобальные переменные неявно инициализируются. Анализ по умолчанию следует Стандарту и рассматривает эту неявную инициализацию.

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

Настройки

На

Polyspace игнорирует неявную инициализацию глобальных и статических переменных. Верификация генерирует ошибку красного Non-initialized variable, если ваш код читает глобальную или статическую переменную перед записью в нее.

Если вы включите эту опцию, глобальные переменные считаются неинициализированными, если вы явно не инициализируете их в коде. Обратите внимание, что эта опция переопределяет опцию Variables to initialize (-main-generator-writes-variables) (Polyspace Code Prover). Даже если вы инициализируете переменные с сгенерированным mainэта опция заставляет анализ игнорировать инициализацию.

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

Polyspace рассматривает глобальные переменные и статические переменные как инициализируемые согласно C99 или ISO® Стандарты C++. Для образца значениями по умолчанию являются:

  • 0 для int

  • 0 для char

  • 0,0 для float

Совет

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

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

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