В этом разделе показано, как просмотреть результаты Code Prover в пользовательском интерфейсе десктопных продуктов Polyspace. Чтобы увидеть, как просмотреть результаты в веб-интерфейсе Polyspace Access, смотрите Результаты Interpret Code Prover в веб-интерфейсе Polyspace Access (Polyspace Code Prover Access).
Когда вы открываете результаты Polyspace® Code Prover™ анализ, вы видите список на панели Results List. Список состоит из проверок во время выполнения, нарушений правил кодирования, метрик кода и использования глобальных переменных.
Вы можете сначала сузить особое внимание вашего обзора:
Используйте фильтры в столбцах списка результатов. Например, вы можете фокусироваться на красных проверках.
Организуйте результаты по файлу и функции. Используйте
значок над списком.
Поскольку результаты проверки во время выполнения Code Prover зависят от результатов предыдущих проверок, она помогает проходить проверки во время выполнения от начала до конца функции.
См. также «Фильтрация и группирование результатов» в интерфейсе пользователя Polyspace Desktop. После сужения списка можно начать просмотр отдельных результатов. В этом разделе описывается, как просмотреть результат.
Чтобы начать проверку, выберите результат в списке.
Первый шаг - понять, в чем проблема. Прочитайте сообщение на панели Result Details и связанную строку кода на панели Source.
На данной точке вы можете принять решение об устранении проблемы.
Сообщение состоит из нескольких частей:
Проверьте цвет и значок: См. Code Prover Result и Source Code Colors. При проверках на ошибки времени выполнения:
: Красный цвет указывает на определенную ошибку.
: Orange указывает на возможную ошибку.
: Серый цвет указывает на недостижимый код.
: Зеленый цвет указывает, что определенная ошибка не может произойти.
Описание проверки во время выполнения.
В предыдущем примере проверка определяет, выходит ли индекс массива за пределы границ массива.
Значения, относящиеся к проверке во время выполнения.
В примере сообщение утверждает размер массива (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. Выберите Go To Definition.
Перемещайтесь от функции к ее вызывающим абонентам и тележкам.
Щелкните
значок на панели Result Details. Вы видите функцию, содержащую результат, с ее вызывающими и callees. Щелкните имя вызывающего абонента или вызывающего абонента, чтобы перейти к узлу вызова. Дважды кликните имя, чтобы перейти к определению.
Кроме того, щелкните
значок, чтобы увидеть графическое представление последовательности вызовов, ведущей к результату. Чтобы перейти к функциям в этой последовательности, щелкните узлы в графике.
Перейдите от вызова функции или ключевого слова цикла к ошибке в теле функции или цикла.
Если ошибка возникает только в конкретном вызове функции или определенной итерации цикла, вызов функции или итерация цикла подсвечивается красным цветом. Щелкните правой кнопкой мыши красный вызов функции или ключевое слово цикла. Выберите Go To Cause, если опция доступна.
Перемещайтесь по всем образцам глобальной переменной.
Щелкните
значок на панели Result Details. Смотрите все глобальные переменные в результате и операции чтения/записи на них.
Прежде чем вы начнете ориентироваться по путям в коде, определите, что вы ищете и выберете соответствующий инструмент навигации. Для образца:
Чтобы исследовать проверку Non-initialized variable, можно убедиться, что переменная вообще не инициализирована. Проверьте предыдущие образцы переменной и проверьте, инициализирована ли она.
Чтобы расследовать нарушение MISRA C:2012 Rule 17.7:
The value returned by a function having non-void return type shall be used.
Для других примеров того, что нужно искать, смотрите Проверки во время выполнения Code Prover. После перехода от текущего результата используйте
значок на панели Result Details, чтобы вернуться к этому результату.
При клике лексемы исходного кода, содержащего результат, предыдущий выбор результата на Results List и подробные сведения на панели Result Details не изменяются. Можно сохранить результат в списке результатов и закрепить подробные данные результатов во время навигации в исходном коде. Иногда можно хотеть увидеть результат, связанный с лексемой. Чтобы обновить выбор результата и детали, Ctrl- щелкните лексема или щелкните правой кнопкой мыши и выберите Select Results At This Location.
Если просмотр результата требует более глубокой навигации в исходном коде, можно создать повторяющееся окно исходного кода, которое фокусируется на результате во время навигации в исходном окне исходного кода.
Щелкните правой кнопкой мыши на панели Source и выберите Create Duplicate Code Window. Щелкните правой кнопкой мыши вкладку, показывающую повторяющееся имя файла (заканчивается на -spawn 1) и выберите New Vertical Group.
Выполните шаги навигации в повторяющемся окне файла, пока дефект все еще появится в исходном окне файла. После завершения расследования закройте повторяющееся окно.