-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)
. Даже если вы инициализируете переменные с сгенерированным main
эта опция заставляет анализ игнорировать инициализацию.
Polyspace рассматривает глобальные переменные и статические переменные как инициализируемые согласно C99 или ISO® Стандарты C++. Для образца значениями по умолчанию являются:
0 для int
0 для char
0,0 для float
Статические локальные переменные имеют тот же срок жизни, что и глобальные переменные, хотя их видимость ограничена функцией, где они заданы. Поэтому опция применяется к статическим локальным переменным.
Параметр: -no-def-init-glob |
По умолчанию: Off |
Пример (Code Prover):
Polyspace Code Prover -sources file_name |
Пример (Код Prover Server):
Полипространство -code-prover-server -sources file_name |