-main-generator-writes-variables
)Задайте глобальные переменные, что вы хотите сгенерированный main
инициализировать
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Задайте глобальные переменные, что вы хотите сгенерированный main
инициализировать. Polyspace® полагает, что эти переменные имеют любое значение, позволенное их типом.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Code Prover Verification. Смотрите Зависимости для других опций, которые необходимо также включить.
Командная строка: Используйте опцию -main-generator-writes-variables
. Смотрите информацию о командной строке.
Если вы проверяете модуль или библиотеку, Программа автоматического доказательства Кода генерирует main
функционируйте, если вы не существуете. Если main
существует, анализ использует существующий main
.
Используйте эту опцию, чтобы задать который глобальные переменные сгенерированный main
должен инициализировать.
Значение по умолчанию:
Код С — public
Код С++ — uninit
uninit
C++ только
Сгенерированный main
только инициализирует глобальные переменные, которые вы не инициализировали во время объявления.
none
Сгенерированный main
не инициализирует глобальные переменные.
public
Сгенерированный main
инициализирует все глобальные переменные кроме объявленных с ключевыми словами static
и const
.
all
Сгенерированный main
инициализирует все глобальные переменные кроме объявленных с ключевым словом const
.
custom
Сгенерированный main
только инициализирует глобальные переменные, которые вы задаете. Щелкните, чтобы добавить поле. Введите имя глобальной переменной.
Можно использовать эту опцию, только если следующее верно:
Ваш код не содержит main
функция.
Опция отключена, если вы включаете опции Ignore default initialization of global variables (-no-def-init-glob)
. Глобальные переменные рассматриваются как неинициализированные, пока вы явным образом не инициализируете их в коде.
Параметр: -main-generator-writes-variables |
Значение: uninit | none | public | all | custom= |
Значение по умолчанию: (C) public | (C++) uninit |
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |
Verify module or library (-main-generator)