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