В этом примере показано, как предоставить контекст для верификации кода С. Если вы используете опции по умолчанию и не предоставляете main функция, Polyspace® Code Prover™ проверяет ваш код на робастность с учетом всех условий верификации. Для образца, программное обеспечение:
Считает, что глобальные переменные и входы незакрытых функций являются полной областью значений.
Генерирует main который вызывает незакрытые функции в произвольном порядке.
В сложение, если вы не задаете функцию, но объявляете и вызываете ее в своем коде, Polyspace заглушает функцию. Подробный список допущений см. в разделе Допущения анализа Code Prover.
Можно использовать опции анализа на панели Configuration, чтобы изменить поведение по умолчанию и предоставить больше контекста о коде. Выполнение контекстной верификации может привести к более проверенному коду и, следовательно, к меньшему количеству оранжевых проверок.
Используйте следующие опции. В пользовательском интерфейсе десктопных продуктов Polyspace опции появляются под узлом Code Prover Verification.
| Опция | Цель |
|---|---|
Variables to initialize (-main-generator-writes-variables) | Задайте глобальные переменные, которые Polyspace должен считать инициализированными, несмотря на отсутствие явной инициализации в коде. |
Constraint setup (-data-range-specifications) | Задайте область значений для глобальных переменных. |
Используйте следующие опции. В пользовательском интерфейсе десктопных продуктов Polyspace опции появляются под узлом Code Prover Verification.
| Опция | Цель |
|---|---|
Initialization functions (-functions-called-before-main) | Задайте функции, которые сгенерированы main должен сначала позвонить. |
Functions to call (-main-generator-calls) | Задайте функции, которые сгенерированы main необходимо позвонить позже. |
Используйте следующие опции. В пользовательском интерфейсе десктопных продуктов Polyspace опции появляются под узлом Inputs & Stubbing.
| Опция | Цель |
|---|---|
Functions to stub (-functions-to-stub) | Задайте функции, которые Polyspace должен заглушить. |
