Оранжевая проверка указывает, что Polyspace® обнаруживает возможную ошибку времени выполнения, но не может доказать его. Чтобы помочь Polyspace привести к более доказанным результатам, вы можете:
Задайте соответствующие опции верификации.
Примените соответствующие методы кодирования.
Можно также ограничить номер и семейство оранжевых проверок, отображенных на Results List. Для получения дополнительной информации смотрите Предельное Отображение Оранжевых Проверок.
Можно принять один или несколько следующих мер для оранжевого сокращения проверки.
Этот пример показывает, как предоставить дополнительную информацию о подписании во время выполнения вашего кода. Иногда, код, который вы предоставляете, не содержит эту информацию. Например:
У вас нет функции main
У вас есть функция, которая объявлена, но не задана.
У вас есть аргументы функции, значения которых доступны только во времени выполнения.
У вас есть одновременно рабочие функции, которые предназначаются для выполнения в определенной последовательности.
Без достаточной информации Polyspace Code Prover™ не может проверить присутствие или отсутствие ошибок времени выполнения.
Можно часто обращаться к объему оранжевых проверок путем ограничения относительно меньшего количества количества оранжевых источников.
В ваших результатах верификации вы видите список источников, таких как энергозависимые переменные и заблокированные функции, которые могут вызвать несколько оранжевых проверок. Чтобы видеть этот список, нажмите
кнопку на панели Result Details. Ограничьте эти источники так, чтобы можно было удалить большинство оранжевых проверок из сверхприближения. В дальнейшей перспективе, вместо того, чтобы реагировать на оранжевые источники во время анализа и ограничить их для более позднего выполнения, разработайте эффективную стратегию для ограничения вероятных оранжевых источников во время самого первого показа.
Смотрите Оранжевые Источники для типов оранжевых источников и как ограничить их.
Чтобы обеспечить больше контекста для верификации и уменьшать оранжевые проверки, используйте эти методы.
| Метод | Пример |
|---|---|
Задайте, как main, сгенерированный Polyspace, инициализирует переменные и вызывает функции | Верификация программы автоматического доказательства кода |
| Задайте области значений для глобальных переменных и аргументов функции. | Создайте ограничительный шаблон из результатов анализа программы автоматического доказательства кода |
| Задайте последовательность выполнения для многозадачного кода. | Конфигурирование анализа многозадачности Polyspace вручную |
| Сопоставьте неточно анализируемую функцию со стандартной функцией для точных результатов на сайтах вызова функции. | -function-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 | Подмножества цели качества программного обеспечения (AGC AC) |
| Рукописный Код С++ | Check MISRA C++ rules | Подмножества цели качества программного обеспечения (C++) |
Из опции выпадающий список выберите SQO-subset1 или SQO-subset2.
Запустите верификацию и рассмотрите ваши результаты.
Зафиксируйте нарушения правила кодирования.
Иногда, размер приложения вызывает потерю точности.
В относительно малом приложении Программа автоматического доказательства Кода сохраняет более точную информацию о переменных диапазонах. Например, предположите, что переменная принимает эти значения: {-2,-1,2,10,15,16,17}. Если эта переменная является знаменателем в делении, Программа автоматического доказательства Кода показывает зеленый Division by zero, пока это сохраняет эту точную информацию. Если размер приложения растет после определенного предела, чтобы уменьшать вычислительную сложность, Программа автоматического доказательства Кода аппроксимирует эту область значений к, например, {-2,2} U {10} U {15,17}. Теперь, если переменная используется для деления, Программа автоматического доказательства Кода показывает оранжевый Division by zero.
Чтобы улучшить точность, можно разделить приложение на несколько модулей. Проверьте каждый модуль независимо от других модулей. Можно рассмотреть полные результаты для одного модуля, в то время как верификация других модулей все еще запускается.
Можно позволить программному обеспечению построить приложение из модулей. Программное обеспечение делит ваши исходные файлы на несколько модулей, таким образом, что взаимозависимость между модулями как можно меньше. Чтобы начаться, выберите Tools> Run Modularize.
Если при запуске верификацию в пользовательском интерфейсе, можно создать несколько модулей в проекте и скопировать исходные файлы в те модули.
Можно выполнить верификацию файла файлом. Каждый файл составляет модуль отдельно. Смотрите Verify files independently (-unit-by-unit).
