-main-generator-writes-variables)Задайте глобальные переменные, что вы хотите сгенерированный main инициализировать
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Эта опция не доступна для кода, сгенерированного из кода MATLAB® или моделей Simulink®.
Задайте глобальные переменные, что вы хотите сгенерированный 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). Глобальные переменные рассматриваются как неинициализированные, пока вы явным образом не инициализируете их в коде.
Эта опция только влияет на глобальные переменные, которые заданы в проекте. Если глобальная переменная объявляется как extern, анализ полагает, что переменная может иметь любое значение, позволенное его типом данных, независимо от значения этой опции.
Параметр: -main-generator-writes-variables |
Значение: uninit | none | public | all | custom= |
Значение по умолчанию: (C) public | (C++) uninit |
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |
Verify module or library (-main-generator)