Polyspace® Code Prover™ проверяет код C/C + + исчерпывающе и доказывает отсутствие определенных типов ошибок времени выполнения (статический анализ или верификация). Что бы вы ни использовали для выполнения анализа, после этого вы открываете результаты в пользовательском интерфейсе Polyspace (или, если вы запустили анализ в Eclipse™, результаты открываются в Eclipse).
Чтобы следовать шагам в этом руководстве, запустите Polyspace с помощью шагов в Run Polyspace Code Prover on Desktop. Кроме того, в пользовательском интерфейсе Polyspace откройте результаты примера с помощью Help > Examples > Code_Prover_Example.psprj. Если вы загрузили результаты примера раньше и внесли некоторые изменения, чтобы загрузить свежую копию, выберите Help > Examples > Restore Default Examples. |
Проверьте каждый результат Polyspace. Найдите первопричину проблемы.
Начните со списка результатов на панели Results List.
Если панель Results List охватывает все окно, выберите Window > Reset Layout > Results Review.
Если вы не видите плоский список результатов, но вместо этого видите их сгруппированными, из
списка выберите None.
Щелкните заголовок Family столбца, чтобы отсортировать результаты на основе того, насколько они критичны. Выберите красный цвет Illegally dereferenced pointer сдайте файл на хранение example.c. Красная проверка указывает, что ошибка происходит на всех путях выполнения, рассматриваемых в анализе.
См. исходный код на панели Source и дополнительные сведения о результате на панели Result Details.
Для Illegally dereferenced pointer результата сообщение на панели Result Details указывает, что указатель p имеет разрешенный буфер 400 байт. Он указывает на место, которое начинается с 400 байтов от начала буфера и указывает на тип данных 4 байта.
Чтобы продолжить расследование и найти первопричину проблемы, щелкните правой кнопкой мыши переменную p на панели Source и выберите Search For All References. Щелкните каждый результат поиска, чтобы перейти к соответствующему местоположению на исходном коде. В каждом месте установите курсор на переменную p чтобы увидеть подсказку, которая описывает значение переменных в этой точке кода.
Вы видите, что переменная указателя p инициализируется в 100-элементный int массив. Указатель пересекает массив в for цикл со 100 итерациями и указывает на конец массива. На линию с проверкой красного Illegally dereferenced pointer этот указатель разыменовывается, что приводит к разыменованию местоположения памяти вне массива.
См.:
Как только вы понимаете первопричину нахождения Polyspace, можно исправить код. В противном случае добавьте комментарии к результатам Polyspace, чтобы исправить код позже или обосновать результат. Можно использовать комментарии для отслеживания прогресса проверки.
Щелкните правой кнопкой мыши переменную p на панели Source. Выберите Open Editor. Код откроется в текстовом редакторе. Устраните проблему. Например, вы можете сделать указатель на начало массива после for цикл. Изменения в коде выделены ниже.
...
int i, *p = array;
for (i = 0; i < 100; i++) {
*p = 0;
p++;
}
p = array;
if (get_bus_status() > 0)
...Кроме того, если вы не хотите немедленно исправлять дефект, присвойте To investigate статуса результату. Вы можете добавить комментарии с дополнительным объяснением.
Если вы присваиваете No action planned статуса, результат не появляется в последующих запусках того же проекта.
См.:
Когда вы открываете результаты анализа Code Prover, вы видите список проверок во время выполнения, нарушений правил кодирования или других результатов. Чтобы организовать проверку, можно сузить список или группу результатов по файлам или типам результатов.
Для образца можно:
Просмотрите только проверки красного и критического оранжевого цвета.
Щелкните заголовок Family столбца, чтобы отсортировать проверки по цвету. Кроме того, можно отфильтровать результаты, отличные от красных и оранжевых проверок. Чтобы начать фильтрацию, щелкните
значок в заголовке столбца.
Можно просмотреть только оранжевые проверки, связанные с путями, поскольку они могут быть более критичными. Чтобы отфильтровать другие проверки, используйте фильтры в столбце Information. Очистите All фильтр и выберите Origin: Path related issue фильтра.
Просмотрите только новые результаты с момента последнего анализа.
На панели инструментов Results List нажмите кнопку New.
Просмотрите результаты в определенных файлах или функциях.
На панели инструментов Results List выберите из списка File.
См.: