Эта тема фокусируется на Polyspace® настольный пользовательский интерфейс. Чтобы узнать об эквивалентной панели в Polyspace доступ к веб-интерфейсу, смотрите Инструментальную панель в Polyspace доступ к веб-интерфейсу.
Панель Dashboard в пользовательском интерфейсе Polyspace обеспечивает статистику по результатам верификации в графическом формате.
На этой вкладке можно просмотреть четыре графика и графики.
Этот график столбца отображения:
Процент файлов проверяется на (проверенные) ошибки времени выполнения. Вы видите этот процент в столбце Files.
Процент функций в проверенных файлах, которые проверяются на (проверенные) ошибки времени выполнения. Вы видите этот процент в столбце Functions.
Процент элементарных операций в проверенных функциях, которые проверяются на ошибки времени выполнения. Вы видите этот процент в столбце Code operations.
Кликните по графику столбца, чтобы открыть окно Unreachable functions.
Это окно содержит:
Количество функций, которые недостижимы в формате, Number of unreachable functions/Total number of functions
Список недостижимых функций наряду с номером документа и номером строки, где они заданы. Выбор функции отображает функциональное определение в панели Source.
Низкое покрытие может указать на раннюю красную проверку или недостающий вызов функции. Рассмотрите следующий код:
void coverage_eg(void)
{
int x;
x = 1 / x;
x = x + 1;
propagate();
}
x — смотрите линию 5. Программное обеспечение не отображает проверки на эти элементарные операции:
Division by zero проверяет деление.
Overflow проверяет результат деления.
Overflow проверяет результат сложения.
Проверка Non-initialized local variable, когда x читается в операции x=x+1.
Когда программное обеспечение отображает только один из пяти проверок операции на код, процент элементарных покрытых операций является 1/5 или 20%. Программное обеспечение не учитывает проверки в недостижимом функциональном propagate(). Для получения дополнительной информации видьте Основания для Кода Непроверенного.
Эта круговая диаграмма отображает количество проверок каждого цвета. Для описания цветов проверки смотрите Цвета Результата и Исходного кода Code Prover.
Используя эту круговую диаграмму, можно получить оценку:
Количество проверок, чтобы рассмотреть.
Селективность вашей верификации — часть проверок, которые не являются оранжевыми.
Можно следовать определенным правилам кодирования или задать определенные опции верификации, чтобы сократить количество оранжевых проверок. Смотрите Уменьшают Оранжевые Регистрации Polyspace Code Prover.
Оранжевый источник является переменной или функцией, которая приводит к оранжевой проверке. Этот график столбца отображает пять оранжевых источников, влияющих на большую часть количества проверок.
Оранжевый источник может вызвать несколько оранжевых регистраций Code Prover. Когда вы кликаете по оранжевому источнику в этом графике, панель Results List показывает только оранжевые проверки, прибывающие из этого источника.
Например, в этом коде, неизвестное значение input может вызвать переполнение и деление на нуль. Переменная input оранжевый источник, который вызывает две оранжевых проверки.
void func (int input) {
int val1;
double val2;
val1 = input++;
val2 = 1.0/input;
}Каждый столбец представляет оранжевый источник. Столбцы располагаются в порядке количества затронутых проверок. Высота столбца указывает на количество проверок, затронутых соответствующим оранжевым источником. Установите свой курсор на столбец, чтобы открыть подсказку, показывающую исходное имя и количество проверок, затронутых источником.
Используя этот график, вы можете:
Просмотрите эти пять источников, влияющих на большую часть количества проверок. Выберите столбец, чтобы посмотреть более подробные детали соответствующего оранжевого источника в панели Orange Sources.
Приоритизируйте свой анализ оранжевых проверок. Если существуют источники, влияющие на большое количество оранжевых проверок, обращаются к тем источникам, если это возможно, прежде чем вы начнете систематический анализ оранжевых проверок. Смотрите Создают Ограничительный Шаблон из Результатов анализа Code Prover.
Этот график столбца отображает пять наиболее нарушенных правил кодирования. Каждый столбец представляет правило кодирования и индексируется номером правила. Высота столбца указывает на количество нарушений правила кодирования, представленного тем столбцом.
Можно также выполнить следующие действия с этой панелью:
Выберите элементы на графиках, чтобы отфильтровать результаты панели Results List. Смотрите Результаты Фильтра и Группы в Пользовательском интерфейсе Рабочего стола Polyspace.
Просмотрите настройку, используемую, чтобы получить результат. Выберите ссылку Configuration.
Просмотрите информацию о функциях, которые не достигнуты во время анализа. Выберите ссылку Unreachable functions.
Просмотрите аналитические предположения позади результата. Выберите ссылку Analysis assumptions.
Просмотрите моделирование многозадачной настройки вашего кода. Выберите ссылку Concurrency modeling.