Verify whole application

Остановите верификацию, если файлы источников являются неполными и не содержат main функция

Описание

Эта опция влияет только на анализ Code Prover.

Эта опция недоступна для кода, сгенерированного из MATLAB® код или Simulink® модели.

Задайте, что Polyspace® верификация должна быть остановлена, если main функция отсутствует в исходных файлах.

Если вы выбираете Visual C++® настройка для Compiler (-compiler)можно указать, какая функция должна рассматриваться как main. См. Main entry point (-main).

Задать опцию

Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция находится на узле Code Prover Verification.

Командная строка и файл опций: Нет соответствующей опции командной строки. См. «Информация о командной строке».

Настройки

На

Верификация Polyspace останавливается, если она не находит main функция в исходных файлах.

Off (по умолчанию)

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 если он не может найти его в исходных файлах.