Остановите верификацию, если исходные файлы являются неполными и не содержат main функция
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Эта опция не доступна для кода, сгенерированного из кода MATLAB® или моделей Simulink®.
Укажите, что верификация Polyspace® должна остановиться если main функция не присутствует в исходных файлах.
Если вы выбираете Visual C ++® устанавливающий для Compiler (-compiler), можно задать, какая функция должна быть рассмотрена как main. Смотрите Main entry point (-main).
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Code Prover Verification.
Командная строка и файл опций: нет никакого соответствующего параметра командной строки. Смотрите информацию о Командной строке.
OnВерификация Polyspace останавливается, если она не находит main функция в исходных файлах.
От (значения по умолчанию)Polyspace продолжает верификацию даже когда main функция не присутствует в исходных файлах. Если main не присутствует, это генерирует файл __polyspace_main.c это содержит main функция.
Если вы используете эту опцию, ваш код должен содержать main функция. В противном случае вы видите ошибку:
Error: required main procedure not found
Если ваш код не содержит main функция, используйте опцию Verify module or library (-main-generator) сгенерировать main функция.
В отличие от пользовательского интерфейса, по умолчанию, останавливается верификация из командной строки, если это не находит main функция в исходных файлах. Если вы задаете опцию -main-generator, Polyspace генерирует main если это не может найти один в исходных файлах.
Verify module or library (-main-generator) | Show global variable sharing and usage only (-shared-variables-mode) (Polyspace Code Prover)
