Остановите верификацию, если исходные файлы являются неполными и не содержат функцию main
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Укажите, что верификация Polyspace® должна остановиться, если функция main не присутствует в исходных файлах.
Если вы выбираете Visual C ++® устанавливающий для Compiler (-compiler), можно задать, какая функция должна быть рассмотрена как main. Смотрите Main entry point (-main).
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Code Prover Verification.
Командная строка: нет никакого соответствующего параметра командной строки. Смотрите информацию о Командной строке.
НаВерификация Polyspace останавливается, если она не находит функцию main в исходных файлах.
От (значения по умолчанию)Polyspace продолжает верификацию, даже когда функция main не присутствует в исходных файлах. Если main не присутствует, он генерирует файл __polyspace_main.c, который содержит функцию main.
В отличие от пользовательского интерфейса, по умолчанию, останавливается верификация из командной строки, если это не находит функцию main в исходных файлах. Если вы задаете опцию -main-generator, Polyspace генерирует main, если это не может найти один в исходных файлах.
Verify module or library (-main-generator)
