В этом разделе показано, как просмотреть результаты проверки кода в пользовательском интерфейсе настольных продуктов Polyspace. Сведения о том, как просматривать результаты в веб-интерфейсе Polyspace Access, см. в разделе Интерпретация результатов проверки кода в веб-интерфейсе Polyspace Access (Polyspace Code Prover Access).
При открытии результатов анализа Prover™ кода Polyspace ® на панели «Список результатов» отображается список. Список состоит из проверок времени выполнения, нарушений правил кодирования, метрик кода и использования глобальных переменных.
Сначала можно сузить фокус обзора:
Используйте фильтры в столбцах списка результатов. Например, можно сосредоточиться на красных чеках.
Упорядочить результаты по файлам и функциям. Используйте
значок над списком.
Поскольку результаты проверки времени выполнения программы Code Prover зависят от результатов предыдущих проверок, она помогает проходить проверку времени выполнения от начала до конца функции.
См. также раздел Фильтрация и группирование результатов в пользовательском интерфейсе Polyspace Desktop. После сужения списка можно начать просмотр отдельных результатов. В этом разделе описывается, как просмотреть результат.
Чтобы начать проверку, выберите результат в списке.
Первый шаг - понять, в чем проблема. Прочитайте сообщение на панели Сведения о результатах и соответствующую строку кода на панели Источник.
На данном этапе вы можете принять решение о том, следует ли устранить проблему.
Сообщение состоит из нескольких частей:
Проверьте цвет и значок: См. Результат проверки кода и цвета исходного кода. В случае проверки на наличие ошибок во время выполнения:
: Красный цвет указывает на определенную ошибку.
: Оранжевый указывает на возможную ошибку.
: Серый указывает на недоступный код.
: Зеленый цвет указывает на невозможность возникновения определенной ошибки.
Описание проверки времени выполнения.
В предыдущем примере проверка определяет, выходит ли индекс массива за границы массива.
Значения, относящиеся к проверке времени выполнения.
В этом примере в сообщении указывается размер массива (127), границы массива (0.. 126) и диапазон значений, которые переменная индекса массива может принимать в этот момент в коде (0.. 555).
Соответствующие источники неточности (для оранжевых чеков).
В этом примере в сообщении указывается, что за проверку могут отвечать две изменчивые переменные.
На панели Источник (Source) переменные и операции с подсказками подчеркнуты.
В этом примере всплывающие подсказки отображаются на:
s8_ret: Вы видите его тип данных и диапазон значений перед + операция.
Если преобразование типа данных происходит во время операции +, это преобразование также отображается во всплывающей подсказке.
+: Вы видите значение левого и правого операнда, и результат.
=: Вы видите любое преобразование типа данных, которое происходит во время назначения и результат.
Иногда для получения определенных результатов требуется дополнительная помощь. Чтобы открыть страницу справки для выбранного результата, щелкните
значок. См. примеры кода, иллюстрирующие результат.
Иногда основная причина может быть далека от фактического местоположения, где отображается результат. Например, считанная переменная может не быть инициализирована, так как инициализация недоступна. Дефект отображается при чтении переменной, но основной причиной может быть предыдущая if или while условие, которое всегда является ложным.
Иногда на панели Сведения о результате (Result Details) отображается одна последовательность событий, которые приводят к результату. Однако в большинстве ситуаций приходится находить собственные пути навигации через код. С помощью подсказок по переменным следите за распространением диапазонов переменных при навигации по коду.
int func (int var) { /* Initial range of var */
…
var -= get (); /* New range of var */
…
set(&var); /* New range of var */
}
Используйте следующие пути быстрой навигации в интерфейсе пользователя:
Выполните поиск всех ссылок на переменную и просмотрите их.
Щелкните правой кнопкой мыши имя переменной на панели Источник (Source) и выберите Поиск всех привязок (Search For All References). Либо дважды щелкните переменную. Эти параметры выполняют более чем строковое соответствие. Параметры показывают только экземпляры определенной переменной, но не другие переменные с таким же именем в других областях.
Перейдите от вызова функции к ее определению.
Щелкните правой кнопкой мыши имя функции на панели Источник (Source). Выберите «Перейти к определению».
Переход от функции к вызывающим и вызываемым абонентам.
Щелкните
значок на панели Сведения о результате (Result Details). Появится функция, содержащая результат, с вызывающими и вызываемыми абонентами. Щелкните имя вызывающего или вызываемого абонента для перехода к узлу вызова. Дважды щелкните имя, чтобы перейти к определению.
Либо щелкните
значок, чтобы увидеть графическое представление последовательности вызовов, приводящее к результату. Чтобы перейти к функциям в этой последовательности, щелкните узлы на графике.
Переход от вызова функции или ключевого слова цикла к ошибке в функции или теле цикла.
Если ошибка возникает только при вызове определенной функции или итерации определенного цикла, вызов функции или итерация цикла подсвечиваются красным цветом. Щелкните правой кнопкой мыши по красному ключевому слову вызова функции или цикла. Выберите «Перейти к причине», если опция доступна.
Навигация по всем экземплярам глобальной переменной.
Щелкните
значок на панели Сведения о результате (Result Details). Просмотрите все глобальные переменные в результатах и операции чтения/записи для них.
Прежде чем начать навигацию по путям в коде, определите, что вы ищете, и выберите соответствующий инструмент навигации. Например:
Для проверки неинициализированной переменной может потребоваться убедиться, что переменная не инициализирована вообще. Найдите предыдущие экземпляры переменной и проверьте, инициализирована ли она.
Расследование нарушения MISRA C:2012 Правило 17.7:
The value returned by a function having non-void return type shall be used.
Другие примеры поиска см. в разделе Проверки времени выполнения средства проверки кода. После перехода от текущего результата используйте
значок на панели Сведения о результате (Result Details), чтобы вернуться к этому результату.
Если щелкнуть маркер исходного кода, содержащий результат, предыдущий выбор результата на панели Список результатов (Results List) и сведения на панели Сведения о результате (Result Details) не изменяются. При навигации по исходному коду можно сохранить результат в списке результатов и сведения о результатах. Иногда может потребоваться просмотреть результат, связанный с маркером. Чтобы обновить выбор результата и подробные данные, Ctrl- щелкните маркер или щелкните правой кнопкой мыши и выберите Выбрать результаты в этом расположении.
Если просмотр результата требует более глубокой навигации в исходном коде, можно создать дублирующееся окно исходного кода, которое фокусируется на результате во время навигации в окне исходного исходного кода.
Щелкните правой кнопкой мыши на панели «Источник» и выберите «Создать окно повторяющегося кода». Щелкните правой кнопкой мыши вкладку с повторяющимся именем файла (заканчивается на -spawn 1) и выберите «Создать вертикальную группу».
Выполните шаги навигации в дублирующемся окне файла, пока дефект все еще отображается в исходном окне файла. После завершения расследования закройте дублирующее окно.