-main-generator)Сгенерируйте функцию main, если исходные файлы являются модулями или библиотеками, которые не содержат main
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Укажите, что Polyspace® должен сгенерировать функцию main, если он не находит один в исходных файлах.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Code Prover Verification.
Командная строка: Используйте опцию -main-generator. Смотрите информацию о Командной строке.
Для аналогичной опции для образцового сгенерированного кода смотрите Verify model generated code (-main-generator).
Используйте эту опцию, если вы проверяете модуль или библиотеку. Анализ Программы автоматического доказательства Кода требует функции main. При проверке модуля или библиотеки, код не может иметь main.
Когда вы используете эту опцию, Программа автоматического доказательства Кода генерирует функцию main, если вы не существуете. Если 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 полагает, что глобальные переменные могут быть записаны между двумя последовательными вызовами функции. Поэтому в каждой вызванной функции, глобальные переменные первоначально имеют полный спектр значений, позволенных их типом.
'off'Polyspace останавливается, если функция main не присутствует в исходных файлах.
Если функция main присутствует в ваших исходных файлах, верификация использует ту функцию main, независимо от того, разрешаете ли вы или отключаете эту опцию.
Опция релевантна, только если функция main не присутствует в ваших исходных файлах.
Если вы задаете многозадачные опции, верификация игнорирует ваши спецификации для генерации main. Вместо этого верификация вводит пустую функцию main.
Для получения дополнительной информации о многозадачных опциях смотрите Анализ Многозадачности Polyspace Конфигурирования Вручную.
Параметр: -main-generator |
| Значение по умолчанию: 'off' |
Пример (программа автоматического доказательства кода):
|
Пример (код доказывают сервер):
|
Class (-class-analyzer) | Functions to call (-main-generator-calls) | Functions to call within the specified classes (-class-analyzer-calls) | Initialization functions (-functions-called-before-main) | Variables to initialize (-main-generator-writes-variables) | Verify whole application