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