В этом примере показано, как предоставить контекст для проверки кода C++. Если вы используете параметры по умолчанию и не предоставляете main функция Polyspace ® Code Prover™ проверяет код на надежность по всем условиям проверки. Например, программное обеспечение:
Считает, что глобальные переменные и входные данные незакрытых функций и методов являются полным диапазоном.
Создает main который вызывает незакрытые функции в произвольном порядке.
Кроме того, если функция не определена, а объявлена и вызвана в коде, Polyspace блокирует функцию. Подробный список допущений см. в разделе Допущения анализа проверочных кодов.
Параметры анализа на панели Конфигурация (Configuration) можно использовать для изменения поведения по умолчанию и предоставления дополнительных контекстных сведений о коде. Выполнение контекстной проверки может привести к более проверенному коду и, следовательно, к меньшему количеству проверок оранжевого цвета.
Используйте следующие опции. В пользовательском интерфейсе настольных продуктов Polyspace параметры отображаются в узле Проверка проверочного кода.
| Выбор | Цель |
|---|---|
Variables to initialize (-main-generator-writes-variables) | Укажите глобальные переменные, которые Polyspace должен считать инициализированными, несмотря на отсутствие явной инициализации в коде. |
Constraint setup (-data-range-specifications) | Укажите диапазон для глобальных переменных. |
Для вызова методов классов используйте следующие опции. В пользовательском интерфейсе настольных продуктов Polyspace параметры отображаются в узле Проверка проверочного кода.
| Выбор | Цель |
|---|---|
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 параметры отображаются в узле Проверка проверочного кода.
| Выбор | Цель |
|---|---|
Initialization functions (-functions-called-before-main) | Укажите функции, созданные main должен позвонить первым. |
Functions to call (-main-generator-calls) | Укажите функции, созданные main должен позвонить позже. |