Остановите верификацию, если исходные файлы являются неполными и не содержат 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 если это не может найти один в исходных файлах.