Polyspace ® Code Prover™ тщательно проверяет код C/C + + и доказывает отсутствие некоторых типов ошибок времени выполнения (статический анализ или проверка). Что бы вы ни использовали для выполнения анализа, после этого вы открываете результаты в интерфейсе пользователя Polyspace (или, если вы выполнили анализ в Eclipse™, результаты открываются в Eclipse).
Для выполнения действий, описанных в этом учебном пособии, запустите программу Polyspace, используя шаги, описанные в разделе Запуск программы проверки кода Polyspace на рабочем столе. Кроме того, в интерфейсе пользователя Polyspace откройте результаты примера с помощью меню «Справка» > «Примеры» > «Code_Prover_Example.psprj». Если ранее были загружены результаты примера и внесены некоторые изменения, для загрузки новой копии выберите «Справка» > «Примеры» > «Восстановить примеры по умолчанию». |
Просмотрите каждый результат Polyspace. Найдите первопричину проблемы.
Начните со списка результатов на панели Список результатов (Results List).
Если панель Список результатов (Results List) охватывает все окно, выберите меню Окно (Window) > Сбросить макет (Reset Layout) > Обзор результатов (Results Review).
Если плоский список результатов не отображается, а вместо этого отображаются сгруппированные результаты,
выберите в списке Нет (None).
Щелкните заголовок столбца «Семейство», чтобы отсортировать результаты по степени их критичности. Отметьте в файле красный флажок «Незаконно отменить ссылку на указатель» example.c. Красная проверка показывает, что ошибка происходит на всех путях выполнения, рассмотренных в анализе.
См. исходный код на панели Источник (Source) и дополнительные сведения о результате на панели Сведения о результате (Result Details).
Сообщение на панели Сведения о результате указывает на то, что для результата «Незаконно удален указатель» p имеет разрешенный буфер 400 байт. Он указывает на местоположение, которое начинается с 400 байт от начала буфера и указывает на тип данных 4 байта.
Для дальнейшего изучения и поиска первопричины проблемы щелкните правой кнопкой мыши переменную. p на панели Источник (Source) и выберите Поиск всех ссылок (Search For All References). Щелкните каждый результат поиска, чтобы перейти к соответствующему местоположению в исходном коде. В каждом месте установите курсор на переменную p для просмотра всплывающей подсказки, описывающей значение переменной в этой точке кода.
Вы видите, что указатель переменной p инициализирован в 100-элементный int массив. Указатель пересекает массив в for цикл со 100 итерациями и указывает на конец массива. В строке с красной галочкой Unlearly derefined pointer этот указатель обнуляется, что приводит к отмене привязки ячейки памяти за пределами массива.
См.:
Как только вы поймете первопричину обнаружения Polyspace, вы сможете исправить код. В противном случае добавьте комментарии к результатам Polyspace, чтобы исправить код позже или оправдать результат. Комментарии можно использовать для отслеживания хода проверки.
Щелкните правой кнопкой мыши переменную p на панели «Источник». Выберите «Открыть редактор». Код открывается в текстовом редакторе. Устраните проблему. Например, можно указать указатель на начало массива после for цикл. Изменения в коде выделены ниже.
...
int i, *p = array;
for (i = 0; i < 100; i++) {
*p = 0;
p++;
}
p = array;
if (get_bus_status() > 0)
...Кроме того, если не требуется немедленно устранять дефект, присвойте результату статус Исследовать. При необходимости добавьте комментарии с дополнительными пояснениями.
При присвоении статуса Нет запланированного действия результат не отображается в последующих прогонах того же проекта.
См.:
При открытии результатов анализа проверки кода отображается список проверок во время выполнения, нарушений правил кодирования или других результатов. Для организации проверки можно сузить список или сгруппировать результаты по типу файла или результата.
Например, можно:
Просмотрите только проверки красного и критического оранжевого цвета.
Щелкните заголовок столбца «Семейство» для сортировки проверок по цвету. Кроме того, можно отфильтровать результаты, отличные от проверки красным и оранжевым. Чтобы начать фильтрацию, щелкните
значок в заголовке столбца.
Можно просмотреть только оранжевые проверки, связанные с путями, поскольку они могут быть более критичными. Чтобы отфильтровать другие проверки, используйте фильтры в столбце Информация (Information). Снимите фильтр Все, а затем выберите фильтр Начало: Проблема, связанная с путем.
Просмотрите только новые результаты с момента последнего анализа.
На панели инструментов панели «Список результатов» нажмите кнопку «Создать».
Просмотр результатов в определенных файлах или функциях.
На панели инструментов панели Список результатов (Results List) в списке выберите Файл (File).
См.: