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