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