В этом примере показано, как обеспечить контекст для вашей верификации кода С. Если вы используете опции по умолчанию и не обеспечиваете main функция, Polyspace® Code Prover™ проверяет ваш код на робастность против всех условий верификации. Например, программное обеспечение:
Полагает, что глобальные переменные и входные параметры невостребованных функций являются полным спектром.
Генерирует main это вызывает невостребованные функции в произвольном порядке.
Кроме того, если вы не задаете функцию, но объявляете и вызываете ее в вашем коде, Polyspace блокирует функцию. Для подробного списка предположений смотрите Аналитические Предположения Программы автоматического доказательства Кода (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. |
