Проверка на оранжевый цвет указывает, что Polyspace® обнаруживает возможную ошибку времени выполнения, но не может ее доказать. Чтобы помочь Polyspace получить более проверенные результаты, можно:
Укажите соответствующие опции верификации.
Следуйте соответствующим практикам кодирования.
Можно также ограничить количество и семейство оранжевых чеков, отображаемых на Results List. Для получения дополнительной информации см. раздел «Предел отображения оранжевых чеков».
Для сокращения оранжевого чека можно выполнить одно или несколько из следующих действий.
В этом примере показано, как предоставить дополнительные сведения о выполнении вашего кода во время выполнения. Иногда код, который вы предоставляете, не содержит этой информации. Для образца:
У вас нет main функция
У вас есть функция, которая объявлена, но не определена.
У вас есть аргументы функции, значения которых доступны только во время выполнения.
У вас есть одновременно выполняемые функции, которые предназначены для выполнения в определенной последовательности.
Без достаточной информации Polyspace Code Prover™ не можете проверить наличие или отсутствие ошибок времени выполнения.
Вы можете часто обращаться к основной массе оранжевых чеков, ограничивая относительно меньшее количество оранжевых источников.
В результатах верификации можно увидеть список источников, таких как изменчивые переменные и упрямые функции, которые могут вызвать несколько оранжевых проверок. Чтобы просмотреть этот список, нажмите
кнопку на панели Result Details. Ограничьте эти источники, чтобы вы могли удалить большинство оранжевых проверок из сверхприближения. В более долгосрочной перспективе вместо того, чтобы реагировать на оранжевые источники во время обзора и ограничивать их для последующего запуска, разработайте эффективную стратегию ограничения вероятных оранжевых источников во время самого первого запуска.
Типы оранжевых источников и способы их ограничения см. в разделе «Источники Orange Checks».
Чтобы предоставить больше контекста для верификации и уменьшить оранжевые проверки, используйте эти методы.
| Метод | Пример |
|---|---|
Определите, как main generated by Polyspace инициализирует переменные и вызывает функции | Верификация Code Prover |
| Задайте области значений для глобальных переменных и аргументов функции. | Создайте шаблон ограничения из результатов анализа Code Prover |
| Задайте последовательность выполнения для многозадачного кода. | Настройка многозадачного анализа Polyspace вручную |
| Сопоставьте неточно проанализированную функцию со стандартной функцией для точных результатов в сайтах вызова функции. | -code-behavior-specifications |
Этот пример показов, как улучшить точность вашей верификации. Повышенная точность уменьшает оранжевые проверки, но увеличивает время верификации.
Используйте следующие опции. В пользовательском интерфейсе Polyspace опции появляются на панели Configuration под узлом Precision.
| Опция | Цель |
|---|---|
Precision level (-O) | Укажите алгоритм верификации. |
Verification level (-to) | Задайте количество раз, когда процесс верификации Polyspace запускается на вашем исходном коде. |
Improve precision of interprocedural analysis (-path-sensitivity-delta) | Распространите большую информацию об аргументах функции в вызываемую функцию. |
Sensitivity context (-context-sensitivity) | Если функция содержит проверку красного и зеленого цвета для одной и той же инструкции от двух различных вызовов, отобразите обе проверки вместо проверки оранжевого цвета. |
В этом примере показано, как следовать правилам кодирования, которые помогают Polyspace Code Prover доказать наличие или отсутствие ошибок времени выполнения. Если ваш код следует определенным подмножествам MISRA® правила кодирования, Polyspace может легче проверить наличие или отсутствие ошибок времени выполнения.
Проверьте, соответствует ли ваш код соответствующему подмножеству правил кодирования.
В пользовательском интерфейсе Polyspace, на панели Configuration, в зависимости от кода, выберите один из опций под узлом Coding Rules.
| Тип кода | Опция | Описание правила |
|---|---|---|
| Рукописный код С | Check MISRA C:2004 или Check MISRA C:2012 | |
| Сгенерированный код C | Check MISRA AC AGC | Целевые подмножества качества программного обеспечения (AC AGC) |
| Рукописный код С++ | Check MISRA C++ rules | Целевые подмножества качества программного обеспечения (C++) |
В раскрывающемся списке опций выберите SQO-subset1 или SQO-subset2.
Запустите верификацию и проверьте результаты.
Исправьте нарушения правил кодирования.
Иногда размер приложения вызывает потерю точности.
В относительно меньшем приложении Кода Prover сохраняет более точную информацию о переменных областях значений. Для образца предположим, что переменная принимает следующие значения: {-2, -1,2,10,15,16,17}. Если эта переменная является знаменателем в делении, Code Prover показывает зеленую Division by zero, пока она сохраняет эту точную информацию. Если размер приложения превышает определенную точку, чтобы уменьшить вычислительную сложность, Код Prover аппроксимирует эту область значений к, для образца, {-2,2} U {10} U {15,17}. Теперь, если переменная используется для деления, Code Prover показывает оранжевую Division by zero.
Для повышения точности можно разделить приложение на несколько модулей. Проверьте каждый модуль независимо от других модулей. Можно просмотреть полные результаты для одного модуля, в то время как верификация других модулей все еще выполняется.
Вы можете позволить программному обеспечению модуляризировать ваше приложение. Программное обеспечение разделяет ваши исходные файлы на несколько модулей таким образом, чтобы взаимозависимость между модулями была как можно меньше. Для начала выберите Tools > Run Modularize.
При запуске верификации в пользовательском интерфейсе можно создать несколько модулей в проекте и скопировать исходные файлы в эти модули.
Можно выполнить верификацию файла по файлам. Каждый файл сам по себе образует модуль. См. Verify files independently (-unit-by-unit).
