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