В этом разделе описываются различные цвета, используемые при отображении результатов анализа Prover™ кода Polyspace ®.
Polyspace отображает различные результаты проверки с определенными значками и цветами на панели Список результатов (Results List) и Сведения о результатах (Result Details).

Средство проверки кода Polyspace проверяет каждую операцию в коде на наличие определенных ошибок времени выполнения. Программа присваивает операции цвет на основании того, доказала ли она существование или отсутствие ошибки времени выполнения на всех или некоторых путях выполнения.
| Проверить цвет | Цель | Пример | Символ |
|---|---|---|---|
|
Красный |
Выделяет операции, которые, как доказано, вызывают определенную ошибку на всех путях выполнения Проверка Polyspace Code Prover определяет ошибки со ссылкой на языковой стандарт. Хотя некоторые ошибки могут быть приемлемыми для конкретной среды компиляции, они нарушают языковой стандарт. Чтобы разрешить некоторое поведение, зависящее от среды, используйте соответствующие опции анализа. Дополнительные сведения см. в разделе Допущения проверки и поведение проверки. |
Переполнение красным цветом на: z = x+y;Операция | |
| Серый |
Выделяет недоступный код. |
Серый Проверка недостижимого кода: if(x>0)
{}
else
{} | |
| Оранжевый |
Выделяет операции, которые могут вызвать ошибку в определенных путях выполнения. Дополнительные сведения см. в разделе Orange Checks in Code Prover. |
Оранжевое переполнение на: z = x+y;Анализ не смог доказать, была ли операция Наиболее распространенной причиной является переполнение операции только для некоторых значений | |
| Зеленый |
Выделяет операции, которые, как доказано, не вызывают определенную ошибку на всех путях выполнения |
Переполнение зеленым цветом на: z = x+y;Операция |
* Для большинства проверок программное обеспечение завершает путь выполнения после первой ошибки времени выполнения на пути. Следовательно, если доказано наличие определенной ошибки (красного цвета) или отсутствие ошибки (зеленого цвета) в операции, подтверждение действительно только для путей выполнения, которые еще не были завершены в этот момент в коде. См. раздел Анализ проверки кода после проверки красного и оранжевого цветов.
Помимо проверки ошибок времени выполнения, программа Polyspace Code Prover также отображает другие результаты о коде.
| Результат | Цель | Символ |
|---|---|---|
| Нарушения правил кодирования | Указывает на нарушение стандартных или пользовательских правил кодирования. | |
| Метрики кода | Указывает метрики сложности кода. | |
| Глобальные переменные | Указывает объявление глобальной переменной. |
Для отображения кода на панели «Источник» в Полиспейсе используется следующая цветовая схема.
Строки с проверками:
Для каждой проверки на панели Список результатов (Results List) Полиспейс (Polyspace) назначает цвет проверки соответствующему разделу кода.
Для строк, содержащих макросы, если макрос свернут, то Polyspace окрашивает всю строку цветом самой строчной проверки на строке. Тяжесть уменьшается в таком порядке: красный, серый, оранжевый, зеленый.
Это недостижимо for цикл содержит макрос MAX_SIZE. Вся линия окрашена в серый цвет.
![]()
Если строка, содержащая макрос, не сдана на хранение, при сворачивании макроса Полиспейс выделяет линию черным цветом.
Для всех остальных строк 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 операторы, в которых макрос для ветви не определен. Этот код не влияет на проверку (или фактическое поведение во время выполнения).

На панели «Доступ к переменным» отображаются глобальные переменные в коде вместе с операциями чтения и записи переменных.
Например, used_global является глобальной переменной, доступ к которой осуществляется четыре раза: один раз во время инициализации, один раз в функции function_with_redи дважды в функции function_with_grey.

Цветовая схема выглядит следующим образом:
Переменные цвета:
Оранжевый: общая, незащищенная глобальная переменная (применяется только к многозадачному коду)
Зеленый: общая защищенная глобальная переменная (применяется только к многозадачному коду)
Черный: не используется совместно, используется глобальная переменная
Серый: Неразделенная, неиспользуемая глобальная переменная
См. раздел Глобальные переменные.
Цвета операций: Если операция происходит в недостижимом коде, она серый, в противном случае черный.
В предыдущем примере одна операция в функции function_with_grey недостижим, но достижим другой.
Дополнительные сведения см. в разделе Переменный доступ.