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