13 / 22
•
если
M
i
— регион элемента массива, то в резюме сохраняется
символьное значение индекса, а результат актуализации — эле-
мент массива от региона, полученного на
(
i
−
1)
-м шаге алгорит-
ма, с символьным значением индекса, определенным в результа-
те актуализации сохраненного значения индекса;
•
если
M
i
— регион поля структуры, то в резюме сохраняется
объявление поля структуры, а результат актуализации — поле
структуры от региона, полученного на
(
i
−
1)
-м шаге алгоритма,
с тем же определением;
•
если
M
i
— регион данных базового класса, то в резюме сохра-
няется ссылка на определение базового класса, а результат ак-
туализации — подрегион данных базового класса от региона,
полученного на
(
i
−
1)
-м шаге, с тем же определением.
Цепочка родительских регионов может строиться как явно — при
построении резюме для региона памяти, так и неявно — при сохра-
нении и последующем разборе символьного значения, для которого
строится резюме.
Применение резюме проверяющими модулями.
Схемы примене-
ния резюме, описанные выше, затрагивают отсечение недостижимых
ветвей выполнения программы и уточнение множества конкретных
значений для символьных значений. Однако для того, чтобы анали-
затор имел возможность выполнять проверки при вложенном вызове
функции, необходима доработка проверяющих модулей. Для получе-
ния проверяющими модулями возможностей анализа при использова-
нии резюме введем две дополнительных функции обратного вызова.
Первая (evalSummaryPopulate) вызывается для сбора резюме прове-
ряющим модулем, вторая (evalSummaryApply) — при применении ре-
зюме.
Проверяющий модуль, имеющий возможность выполнения дей-
ствий при событии SummaryPopulate, должен сохранить информацию,
которая может понадобиться для обновления состояния или выпол-
нения отложенной проверки. Информация, содержащаяся в резюме,
не освобождается до окончания работы анализатора, поэтому прове-
ряющий модуль может использовать произвольный формат хранения
данных, лучшим образом отвечающий задаче проверки. Как показала
практика модификации проверяющих модулей, для каждой провер-
ки, проводимой модулем, в GDM обычно помещается две дополни-
тельных записи, которые затем используются для заполнения резюме:
для обновления состояния и отложенной проверки. В качестве приме-
ра рассмотрим проверку двойного закрытия файлового дескриптора.
В резюме помещаются две секции: первая отвечает за обновление
состояния дескриптора (является ли он открытым или закрытым), а
вторая — за выполнение отложенной проверки (в ней запоминаются
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 5 87