5 / 22
пометка регионов памяти как не содержащих первоначальное значе-
ние (инвалидация) и удаление имеющихся привязок, происходящее
при потере регионом памяти активности, а также иногда используемое
вместо инвалидации. Если необходимо получить символьное значение
для региона памяти, не имеющего записи в модели памяти (например,
для аргументов функции), происходит неявное связывание с помощью
символьного значения специального вида, при этом записи в модели
памяти не создается.
2. Окружение (
Environment
) ставит в соответствие активным выра-
жениям их как левосторонние символьные значения, так и правосто-
ронние (левосторонними значениями выражений являются абстракт-
ные области памяти кода программы, где располагаются выражения, а
правосторонними — вычисленные символьные значения выражений).
3. Нетипизированное хранилище (Generic Data Map, GDM) — кон-
тейнер для хранения данных проверок, а также для хранения некото-
рых специфических структур данных ядра анализатора, связанных с
состоянием программы. Наиболее важными такими данными является
карта соответствия символов и их диапазонов возможных значений,
с помощью которой проводится анализ достижимости. За помеще-
ние данных в GDM и удаление их оттуда отвечают непосредственно
использующие эти данные модули — проверки и модули ядра анали-
затора (в частности, ответственный за арифметические и логические
вычисления решатель ConstraintManager).
Символьное значение в терминологии CSA — это абстракция пе-
ременного или константного значения какого-либо типа данных. Аб-
страктным значением можно представить, например, значение выра-
жения, содержимое области памяти, саму область памяти и указатель
на нее. В модели CSA символьное значение может иметь несколько
основные видов: целочисленная константа; символьное выражение;
регионы памяти.
Эффекты, учитываемые в резюме функции.
Каждый оператор
при выполнении производит эффект, заключающийся в изменении со-
стояния программы. В случае анализа речь идет о моделировании
эффектов операторов, т.е. о моделировании действия, которое модели-
руемый оператор оказывает на модель состояния программы.
С учетом описанной модели анализатора сократить время анали-
за при использовании резюме в сравнении с временем анализа при
применении метода встраивания можно за счет отсутствия необходи-
мости затрачивать время на анализ эффектов, действия которых ло-
кальны или не учитываются при дальнейшем анализе. Так, связыва-
ние символьного значения с выражением имеет только локальный эф-
фект, поскольку все выражения становятся неактивными при выходе
из контекста анализа функции. Аналогично, локальный эффект имеют
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 5 79