Метод резюме для разработки универсального многоцелевого анализатора кодов программ с возможностью обнаружения различных классов дефектов в программах, созданных с использованием языков С и С++

В терминологии CSA, описанной в работе [14], выполнение про-

граммы представляет собой множество последовательных переходов

между состояниями из одного состояния в другие. Каждому состоя-

нию соответствует точка выполнения (ProgramPoint), для которого это

состояние актуально

. Переходы между состояниями обусловлены ли-

бо эффектами интерпретации отдельных выражений, определенными

стандартом языка, либо событиям, связанными с выполнением прове-

рок проверяющими модулями (Checker). Из одной точки выполнения

может идти один и более переход в другое. Несколько переходов про-

исходит в случаях, когда условие перехода невозможно однозначно

разрешить в пользу выбора какой-либо одной ветви выполнения, на-

пример, при обработке условных операторов (это и есть разделение

на классы эквивалентности). Кроме того, проверки также могут разде-

лять состояние программы, сохраняя в разных структурах состояния

различающиеся данные состояния. Результирующее множество узлов

в виде состояний и переходов из одного состояния программы в другое

образует граф выполнения программы (ExplodedGraph).

За базовое моделирование без каких-либо проверок корректности

исходного кода отвечает ядро анализатора. Ядро анализатора пред-

ставляет собой, во-первых, набор методов, связанных с построением

графа состояний выполнения программы (класс CoreEngine), а, во-

вторых, набор методов, отвечающих за моделирование эффектов, спе-

цифичных для языка программирования, т.е. моделирование эффектов

выражений и правил их выполнения (ExprEngine). Кроме того, в про-

цедуре построения графа выполнения могут принимать участие прове-

ряющие модули, анализируя события, которые наступают в процессе

выполнения. Эти проверки могут останавливать построение графа на

заданном пути в случае обнаружения критического дефекта, разделять

состояние программы и вносить в него дополнительную информацию

для работы проверяющего модуля.

Структура состояния — представление состояния программы в точ-

ке выполнения. Структура состояния включает следующие данные.

1. Содержимое памяти программы (модель памяти,

RegionStore

)

[15], представляемое как отображение между регионами памяти и сим-

вольными значениями, связанными с этими регионами. Для создания

записи в модели памяти необходимо провести непосредственное свя-

зывание региона памяти и его значения, например, при обработке опе-

ратора присваивания. Операциями, изменяющими содержимое модели

памяти, являются непосредственное связывание региона со значением

(выполняющееся, например, при присваивании переменной значения),

Здесь и далее в скобках приведены названия соответствующих классов фрейм-

ворка CSA.

78 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 5