-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' |
Пример (Программа автоматического доказательства Кода):
Polyspace Code Prover - источники |
Пример (Код Доказывают Сервер):
сервер программы автоматического доказательства полипробела кода - источники |
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