Up

[Svace] Внутрипроцедурный анализ для поиска ошибок на основе символьного выполнения

[Svace] Внутрипроцедурный анализ для поиска ошибок на основе символьного выполнения
1 · 2 · 3 · 4 — 13

1 Подходы: (1) на основе абстрактного синтаксического дерева, (2) межпроцедурный анализ с моделированием указываемых ячеек памяти, (3) внутрипроцедурный анализ отдельных функций. 2 Анализ неконсервативен (может выдавать некорректные результаты ради скорости или потребления памяти). Символьное выполнение осуществляется в топологическом порядке (что это?). Точки слияния анализируются после всех состояний на входных рёбрах. Выделяются ССК, для них производится несколько (N) итераций цикла. 3 Символы языка — переменные программы. Ai — анализы, Ci — детекторы. Запускаются для каждой вершины. Анализу доступны результаты анализов на входных рёбрах, но недоступны на выходных. 4 Идентификатор значения — абстракция для обозначения разбиения значений переменных на классы эквивалентности (видимо, символьная переменная). Атрибуты используются для описания свойств. 13 Результаты анализов сохраняются в виде атрибутов. Атрибуты: интервалы значений, блокировка мьютекса, интервал длины строки и т. д.

Sergey Vartanov, 2007–2020