В этом примере показано, как предоставить контекст вашей верификации Кода С++. Если вы используете опции по умолчанию и не обеспечиваете 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.
| Опция | Цель |
|---|---|
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 должен вызвать позже. |
