В этом примере показано, как предоставить контекст вашей верификации Кода С++. Если вы используете опции по умолчанию и не обеспечиваете 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.
| Опция | Цель |
|---|---|
Class (-class-analyzer) | Задайте классы чьи методы сгенерированный main должен вызвать. |
Functions to call within the specified classes (-class-analyzer-calls) | Задайте методы что сгенерированный main должен вызвать. |
Analyze class contents only (-class-only) | Укажите что сгенерированный main должен вызвать методы класса только. |
Skip member initialization check (-no-constructors-init-check) | Укажите что сгенерированный main не должен проверять, инициализирует ли каждый конструктор класса все члены класса. |
Используйте следующие опции, чтобы вызвать функции, которые не являются методами класса. В пользовательском интерфейсе десктопных решений Polyspace опции появляются под узлом Code Prover Verification.
| Опция | Цель |
|---|---|
Initialization functions (-functions-called-before-main) | Задайте функции что сгенерированный main должен вызвать сначала. |
Functions to call (-main-generator-calls) | Задайте функции что сгенерированный main должен вызвать позже. |
