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