9 / 22
связанного с данным регионом, в данной ветви выполнения. При этом
первое событие потери активности соответствует диапазону входных
значений, а последнее — диапазону выходных значений, если они сов-
падают, то никаких присваиваний или инвалидаций региона входного
символа не было, входной диапазон также является выходным. Такой
метод позволяет избежать использования сложных алгоритмических
схем для сбора входных и выходных значений аргументов функций,
входных значений глобальных регионов памяти.
Сбор выходных значений иногда требуется проводить по оконча-
нии пути выполнения функции. Это необходимо для обработки сим-
вольных значений, привязанных к региону памяти непосредственным
присваиванием или иным видом связывания. Для этого используется
итерация по хранилищу с сохранением диапазонов внешних по отно-
шении к функции регионов памяти в резюме.
Инвалидация региона памяти в терминологии CSA означает свя-
зывание с данным регионом нового символа без наложенных на него
ограничений, т.е. способного принимать произвольные значения. По-
скольку символьные значения, связанные с регионами памяти, обраба-
тываются при завершающем проходе по хранилищу, а значения регио-
нов, актуальные до инвалидации, обрабатываются по событию потери
активности, непосредственно предшествующему событию связывания
нового значения, инвалидация обрабатывается автоматически, допол-
нительных действий для обработки инвалидаций регионов памяти не
требуется.
Обработка события возврата функцией значения достаточно три-
виальна. Результирующее символьное значение сохраняется в резюме
целиком, а ограничения, накладываемые на него и на его части, обра-
батываются отдельно.
За хранение данных проверок проверяющие модули отвечают са-
мостоятельно. Основными видами данных проверок являются отмет-
ка отложенной проверки и данные состояния проверки. Отложенные
проверки используются для выдачи предупреждений в тех ситуациях,
когда вследствие отсутствия данных о контексте вызова невозможно
однозначно утверждать наличие дефекта или его отсутствие. Данные
состояния необходимы для построения нового состояния проверки при
применении резюме.
Актуализация символьных значений.
В результате сбора резюме
на предыдущем шаге получено некоторое множество регионов памяти,
с которыми связаны некоторые символьные значения. Кроме того, ре-
гионы памяти могут входить в символьные значения как их составная
часть. Однако полученные регионы памяти адресуются в контексте
объявлений имен внутри функции. В контексте вызывающей функции
эти регионы могут иметь уже другое значение, т.е. регионы, исполь-
зуемые внутри функции, являются относительными по отношению к
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 5 83