Polyspace® Code Prover™ проверяет код C/C++ исчерпывающе и доказывает отсутствие определенных типов ошибок времени выполнения (статический анализ или верификация). Безотносительно средних значений вы используете для выполнения анализа, впоследствии, вы открываете результаты в пользовательском интерфейсе Polyspace (или если вы запустили анализ в Eclipse™, результаты, открытые в Eclipse).
Чтобы выполнить шаги в этом примере, запустите Polyspace с помощью шагов в Запущенном Polyspace Code Prover на Коде C/C++. Также в пользовательском интерфейсе 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 инициализируется к массиву int с 100 элементами. Указатель пересекает массив в цикле 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, результат не появляется в последующих выполнениях на том же проекте.
См.:
Когда вы открываете результаты анализа Программы автоматического доказательства Кода, вы видите список проверок на этапе выполнения, кодируя нарушения правила или другие результаты. Чтобы организовать ваш анализ, можно сузить список или результаты группы файлом или закончиться тип.
Например, вы можете:
Рассмотрите только красные и критические оранжевые проверки.
Щелкните заголовок столбца Family к виду проверяет цвет. Также можно отфильтровать результаты кроме красных и оранжевых проверок. Чтобы начать фильтровать, кликните
по значку на заголовке столбца.
Можно рассмотреть только связанные с путем оранжевые проверки, потому что они, вероятно, будут более очень важными. Чтобы отфильтровать другие проверки, используйте фильтры на столбце Information. Очистите фильтр All и затем выберите фильтр Origin: Path related issue.
Рассмотрите только новые результаты начиная с последнего анализа.
На панели инструментов панели Results List нажмите кнопку New.
Рассмотрите результаты в определенных файлах или функциях.
На панели инструментов панели Results List, из списка, выбирают File.
См.: