-no-def-init-glob)Рассмотрите глобальные переменные как неинициализированные, если явным образом не инициализировано в коде
Эта опция применяется к Программе автоматического доказательства Кода только. Это не влияет на анализ Средства поиска Ошибки.
Укажите, что Polyspace® не должен рассматривать глобальные и статические переменные, как инициализировано, если они явным образом не инициализируются в коде.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Inputs & Stubbing.
Командная строка: Используйте опцию -no-def-init-glob. Смотрите информацию о командной строке.
Стандарт C99 указывает, что глобальные переменные неявно инициализируются. Анализ по умолчанию следует Стандарту и рассматривает эту неявную инициализацию.
Если вы хотите инициализировать определенные глобальные переменные явным образом, используйте эту опцию, чтобы найти экземпляры, где глобальные переменные явным образом не инициализируются.
OnPolyspace игнорирует неявную инициализацию глобальных и статических переменных. Верификация генерирует красную ошибку Non-initialized variable, если ваш код читает глобальную или статическую переменную прежде, чем записать в нее.
Если вы включаете эту опцию, глобальные переменные рассматриваются неинициализированными, если вы явным образом не инициализируете их в коде. Обратите внимание на то, что эта опция заменяет опцию Variables to initialize (-main-generator-writes-variables). Даже если вы инициализируете переменные сгенерированным main, эта опция обеспечивает анализ, чтобы проигнорировать инициализацию.
От (значения по умолчанию)Polyspace полагает, что глобальные переменные и статические переменные инициализируются согласно стандартам ISO® C ++ или C99. Например, значения по умолчанию:
0 для int
0 для char
0.0 для float
Статические локальные переменные имеют то же время жизни как глобальные переменные даже при том, что их видимость ограничивается функцией, где они заданы. Поэтому опция применяется к статическим локальным переменным.
Параметр: -no-def-init-glob |
| Значение по умолчанию: Off |
Пример (Программа автоматического доказательства Кода):
Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |