Эта тема объясняет различные цвета, используемые в отображении результатов анализа 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 недостижимо, но другой достижимо.
Для получения дополнительной информации смотрите Переменный доступ.
