-main-generator
)Сгенерируйте main
функция, если исходные файлы являются модулями или библиотеками, которые не содержат main
Эта опция влияет только на анализ Code Prover.
Задайте, что Polyspace® необходимо сгенерировать main
функцию, если она не находит ее в исходных файлах.
Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция находится на узле Code Prover Verification.
Командная строка и файл опций: Используйте опцию -main-generator
. См. «Информация о командной строке».
Для аналогичной опции для сгенерированного моделью кода смотрите Verify model generated code (-main-generator)
.
Используйте эту опцию при проверке модуля или библиотеки. Для анализа Code Prover требуется main
функция. При проверке модуля или библиотеки ваш код может не иметь main
.
Когда вы используете эту опцию, Code Prover генерирует main
функция, если она не существует. Если a main
существует, в анализе используются существующие main
.
Polyspace генерирует main
функцию, если она не находит ее в исходных файлах. Сгенерированный main
:
Инициализирует переменные, заданные Variables to initialize (-main-generator-writes-variables)
.
Перед вызовом других функций вызывает функции, заданные Initialization functions (-functions-called-before-main)
.
Во всех возможных порядках вызываются функции, заданные Functions to call (-main-generator-calls)
.
(Только для C++) Вызывает методы класса, заданные Class (-class-analyzer)
и Functions to call within the specified classes (-class-analyzer-calls)
.
Если вы не задаете функцию и переменные опции выше, сгенерированный main
:
Инициализирует все глобальные переменные, кроме объявленных с ключевыми словами const
и static
.
Во всех возможных порядках вызывает все функции, которые нигде не вызываются в исходных файлах. Polyspace считает, что глобальные переменные могут быть записаны между двумя последовательными вызовами функции. Поэтому в каждой вызываемой функции глобальные переменные первоначально имеют полную область значений значений, разрешенных их типом.
Polyspace останавливает, если main
функция отсутствует в исходных файлах.
Если a main
функция присутствует в ваших исходных файлах, верификация использует это main
function, независимо от того, включите ли вы или отключите эту опцию.
Опция релевантна только в том случае, если main
функция отсутствует в исходных файлах.
Если вы используете опцию Verify whole application
(по умолчанию в командной строке), ваш код должен содержать main
функция. В противном случае вы увидите ошибку:
Error: required main procedure not found
Если ваш код не содержит main
function, используйте эту опцию, чтобы сгенерировать main
функция.
Если вы задаете опции многозадачности, верификация игнорирует ваши спецификации для main
генерация. Вместо этого верификация вводит пустую main
функция.
Дополнительные сведения об опциях многозадачности см. в разделе Настройка многозадачного анализа Polyspace вручную.
Параметр: -main-generator |
По умолчанию: Off |
Пример (Code Prover):
Polyspace Code Prover -sources file_name |
Пример (Код Prover Server):
Полипространство -code-prover-server -sources file_name |