-main-generator-writes-variables)Задайте глобальные переменные, которые вы хотите, чтобы сгенерированный main инициализировал
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Задайте глобальные переменные, которые вы хотите, чтобы сгенерированный main инициализировал. Polyspace® полагает, что эти переменные имеют любое значение, позволенное их типом.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Code Prover Verification. Смотрите Зависимости для других опций, которые необходимо также включить.
Командная строка: Используйте опцию -main-generator-writes-variables. Смотрите информацию о Командной строке.
Если вы проверяете модуль или библиотеку, Программа автоматического доказательства Кода генерирует функцию main, если вы не существуете. Если main существует, анализ использует существующий main.
Используйте эту опцию, чтобы задать, какие глобальные переменные сгенерированный main должен инициализировать.
Значение по умолчанию:
Код С — public
Код С++ — uninit
uninitC++ только
Сгенерированный 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 | |
Значение по умолчанию: (C) public | (C++) uninit |
Пример (программа автоматического доказательства кода): |
Пример (сервер программы автоматического доказательства кода):
|
Verify module or library (-main-generator)