Эта тема показывает, как рассмотреть результаты Программы автоматического доказательства Кода в пользовательском интерфейсе десктопных решений Polyspace. Чтобы видеть, как рассмотреть результаты в Polyspace доступ к веб-интерфейсу, смотрите, Интерпретируют Результаты Программы автоматического доказательства Кода в Polyspace доступ к веб-интерфейсу (Polyspace Code Prover Access).
Когда вы открываете результаты анализа Polyspace® Code Prover™, вы видите список на панели Results List. Список состоит из проверок на этапе выполнения, кодируя нарушения правила, метрики кода и использование глобальной переменной.
Можно сначала сузить особое внимание анализа:
Используйте фильтры на столбцах списка результатов. Например, можно фокусироваться на красных проверках.
Организуйте результаты файлом и функцией. Используйте
значок выше списка.
Поскольку результаты проверки на этапе выполнения Программы автоматического доказательства Кода зависят от результатов предыдущих проверок, она помогает пройти проверки на этапе выполнения с начала в конец функции.
См. также Фильтр и Результаты Группы в Пользовательском интерфейсе Рабочего стола Polyspace. Если вы сужаете список, можно начать рассматривать отдельные результаты. Эта тема описывает, как рассмотреть результат.
Чтобы начать ваш анализ, выберите результат в списке.
Первый шаг должен изучить, какова проблема. Считайте сообщение на панели Result Details и связанную строку кода на панели Source.
На данном этапе вы можете быть готовы решить, устранить ли проблему.
Сообщение состоит из нескольких частей:
Цвет проверки и значок: Смотрите Цвета Результата и Исходного кода Программы автоматического доказательства Кода. В случае проверок на ошибки времени выполнения:
: Красный указывает на определенную ошибку.
: Оранжевый указывает на возможную ошибку.
: Грэй указывает на недостижимый код.
: Грин указывает, что определенной ошибки не может произойти.
Описание проверки на этапе выполнения.
В предыдущем примере проверка определяет, выходит ли индекс массива за пределы границ массивов.
Значения, относящиеся к проверке на этапе выполнения.
В примере сообщение утверждает размер массивов (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. Вы видите, что функция содержит результат с его вызывающими сторонами и вызываемыми. Кликните по имени вызывающей стороны или вызываемого, чтобы перейти на сайт вызова. Дважды кликните имя, чтобы перейти к определению.
В качестве альтернативы кликните
по значку, чтобы видеть графическое представление продвижения последовательности вызова к результату. Чтобы перейти к функциям в этой последовательности, щелкните через узлы в графике.
Перейдите от вызова функции или ключевого слова цикла к ошибке в теле функции или теле цикла.
Если ошибка происходит только в определенном вызове функции или определенной итерации цикла, вызов функции или итерация цикла подсвечены красные. Щелкните правой кнопкой по красному вызову функции или ключевому слову цикла. Выберите 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.
Для других примеров того, что искать, смотрите Проверки на этапе выполнения Программы автоматического доказательства Кода. После того, как вы перейдете далеко от текущего результата, используйте
значок на панели Result Details, чтобы возвратиться к тому результату.
Если вы кликаете по лексеме исходного кода, содержащей результат, предыдущий выбор результата на Results List и детали о панели Result Details не изменяются. Можно сохранить результат в списке результатов и деталях результата прикрепленным при навигации в исходном коде. Иногда, вы можете хотеть видеть результат, сопоставленный с лексемой. Обновить выбор результата и детали, Ctrl- кликните по лексеме или щелкните правой кнопкой и выберите Select Results At This Location.
Если рассматривание результата требует более глубокой навигации в вашем исходном коде, можно создать дублирующееся окно исходного кода, которое фокусируется на результате, в то время как вы перешли в окне первоисточника кода.
Щелкните правой кнопкой по Source, разделяют на области и выбирают Create Duplicate Code Window. Щелкните правой кнопкой по вкладке, показывающей дублирующееся имя файла (заканчивающийся -spawn 1) и выберите New Vertical Group.
Выполните шаги навигации в дублирующемся окне файла, в то время как дефект все еще появляется в исходном окне файла. После того, как расследование завершено, закройте дублирующееся окно.