Эта тема объясняет различные цвета, используемые в отображении результатов анализа Polyspace® Code Prover™.
Polyspace отображает различные результаты верификации с определенными значками и цветами на панели Result Details и Results List.
Polyspace Code Prover проверяет каждую операцию в ваш код для конкретных ошибок времени выполнения. Программное обеспечение присваивает цвет операции на основе того, доказало ли это существование или отсутствие ошибки времени выполнения на всех или некоторых путях к выполнению.
| Проверяйте цвет | Цель | Пример | Значок |
|---|---|---|---|
|
Красный |
Операции подсветок, которые, как доказывают, вызывают конкретную ошибку на всем выполнении paths Верификация Polyspace Code Prover определяет ошибки со ссылкой на стандарт языка. Хотя некоторые ошибки могут быть приемлемыми для конкретной среды компиляции, они нарушают стандарт языка. Чтобы позволить часть зависимого средой поведения, используйте соответствующие аналитические опции. Для получения дополнительной информации смотрите Предположения Верификации и Поведение Проверки. |
Красный Overflow на: z = x+y;Операция |  |
| Серый |
Подсвечивает недостижимый код. |
Серая проверка Unreachable code: if(x>0)
{}
else
{}Ответвление |  |
| Оранжевый |
Операции подсветок, которые могут вызвать ошибку на определенных путях к выполнению. Для получения дополнительной информации смотрите Оранжевые Регистрации Программы автоматического доказательства Кода. |
Оранжевый Overflow на: z = x+y;Анализ не мог доказать, переполняется ли операция Наиболее распространенная причина состоит в том, что операция переполняется только для некоторых значений |  |
| Зеленый |
Операции подсветок, которые, как доказывают, не вызывают конкретную ошибку на всем выполнении paths |
Зеленый Overflow на: z = x+y;Операция | 
|
* Для большинства проверок, программное обеспечение отключает следование траектории выполнения первая ошибка времени выполнения на пути. Поэтому, если это доказывает определенную (красную) ошибку или отсутствие ошибки (зеленой) на операции, доказательство допустимо только для путей к выполнению, которые еще не были отключены в той точке в коде. Смотрите, что Анализ Программы автоматического доказательства Кода Следует за Красными и Оранжевыми Проверками.
Помимо проверок на ошибки времени выполнения, Polyspace Code Prover также отображает другие результаты о вашем коде.
| Результат | Цель | Значок |
|---|---|---|
| Кодирование нарушений правила | Указывает на нарушение предопределенных или пользовательских правил кодирования. |  для предопределенных правил и для пользовательских правил. |
| Метрики кода | Указывает на метрики сложности кода. |  для метрик, которые не превышают предел, который вы задали и для метрик, которые превышают предел. |
| Глобальные переменные | Указывает на объявление глобальной переменной. |  для разделяемых потенциально незащищенных переменных и для неразделяемых неиспользуемых переменных |
Polyspace использует следующую цветовую схему для отображения кода по панели Source.
Строки с проверками:
Для каждого проверять панель Results List, Polyspace присваивает цвет проверки соответствующему разделу кода.
Для строк, содержащих макросы, если макрос сворачивается, то Polyspace окрашивает целую линию с цветом наиболее строгой проверки на строке. Серьезность уменьшается в этом порядке: красный, серый, оранжевый, зеленый.
Этот недостижимый цикл for содержит макро-MAX_SIZE. Целая линия окрашена серый.
Если нет никакой регистрации строки, содержащей макрос, Polyspace подчеркивает строку черного цвета цвета, когда макрос сворачивается.
Для всех других строк Polyspace окрашивает только ключевое слово или идентификатор сопоставленными с проверкой.
Это присвоение имеет три проверки: i и used_global инициализируются, но к массиву tab можно получить доступ вне его границ. Оператор [ окрашен в оранжевый, чтобы указать на проблему.
Строки с кодированием нарушений правила:
Поскольку каждое кодирование управляет нарушением на панели Results List, присвоениях Polyspace к соответствующему ключевому слову или идентификатору:
(Инвертированный треугольник) символ, если правило кодирования является предопределенным правилом. Предопределенными доступными правилами является MISRA C®, MISRA® AC AGC, MISRA C++ или JSF® C ++.
Этот оператор if и операция || нарушают правила MISRA.
Символ, если правило кодирования является пользовательским правилом.
Это имя функции нарушает настраиваемое правило именования.
Строки с подсказками:
Если подсказка доступна для ключевого слова или идентификатора на панели Source, Polyspace:
Подчеркивание тела использования для ключевого слова или идентификатора, если это сопоставлено с проверкой.
Эта строка имеет и проверки и подсказки на input, % и used_global.
Использование подчеркнуло штриховой линией подчеркивание для ключевого слова или идентификатора, если это не сопоставлено с проверкой.
Эта строка имеет подсказки на for и <, но не проверяет их.
Использование подчеркнуло штриховой линией красное подчеркивание на вызовах функции указать, что тело функции содержит определенную ошибку времени выполнения. Подсказка показывает строку в теле функции, которое вызывает ошибку.
Этот вызов function_with_red приводит к ошибке времени выполнения.
Функциональные определения:
Когда функция задана, Polyspace окрашивает синее имя функции.
Строки, деактивированные из-за условной компиляции:
Polyspace присваивает более легкий оттенок серого коду, деактивированному из-за условной компиляции. Такой код происходит, например, в операторах #ifdef, где макрос для ответвления не задан. Этот код не влияет на верификацию.
Панель Variable Access показывает глобальные переменные в вашем коде наряду с операциями чтения и операциями записи на переменных.
Например, used_global является глобальной переменной, к которой получают доступ четыре раза: однажды во время инициализации, однажды в функциональном function_with_red, и дважды в функциональном function_with_grey.
Цветовая схема следующие:
Переменные цвета:
Оранжевый: Разделяемая, незащищенная глобальная переменная (только применимый к многозадачному коду)
Зеленый: Разделяемая, защищенная глобальная переменная (только применимый к многозадачному коду)
Черный: Неразделенная, используемая глобальная переменная
Серый: Неразделенная, неиспользованная глобальная переменная
Смотрите глобальные переменные.
Цвета операции: Если операция происходит в недостижимом коде, это серо, в противном случае черно.
В предыдущем примере одна операция в функциональном function_with_grey недостижима, но другой достижимо.
Для получения дополнительной информации смотрите Переменный доступ.
