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