Введение
1 Методы статического межпроцедурного анализа программ 14
1.1 Методы обеспечения качества ПО. Статический анализ 14
1.2 Существующие средства статического анализа, имеющие поддержку языков C и C++
1.2.1 Коммерческие статические анализаторы 21
1.2.2 Свободно распространяемые статические анализаторы
1.3 Метод анализа программ с помощью символьного выполнения 25
1.4 Межпроцедурный анализ для метода символьного выполнения 30
1.5 Улучшения метода символьного выполнения 32
2 Межпроцедурный анализ на основе резюме для метода символьного выполнения 39
2.1 Математическая модель для оценки временных затрат при встраивании и использовании метода резюме. 39
2.2 Алгоритм метода резюме для символьного выполнения 43
2.3 Модель анализатора
2.3.1 Общая математическая модель системы состояний и переходов в процессе символьного выполнения программы 44
2.3.2 Конкретизация формальной модели для задачи анализа программ 47
2.3.3 Реализация формальной модели 50
2.3.4 Формальное описание процесса межпроцедурного анализа 57
2.3.5 Эффекты, учитываемые в резюме функции 58
2.4 Оценка сложности алгоритмов, реализующих различные методы межпроцедурного анализа 61
2.4.1 Оценка временной сложности реализации анализа методом символьного выполнения без межпроцедурного анализа 62
2.4.2 Оценка временной сложности реализации алгоритма метода встраивания 63
2.4.3 Оценка асимптотической сложности реализации алгоритма разрабатываемого метода, использующего резюме
2.5 Порождение новых ветвей выполнения программы и отсечение недостижимых путей 66
2.6 Сбор данных для создания резюме 68
2.7 Актуализация символьных значений
2.7.1 Регионы, относящиеся к пространству аргументов вызываемой функции 71
2.7.2 Регионы памяти внешней области видимости 72
2.7.3 Актуализация составных и служебных символьных значений 73
2.7.4 Актуализация литеральных регионов
2.8 Применение резюме проверяющими модулями 76
2.9 Исследование особенностей и ограничений разработанного метода
2.9.1 Анализ при наличии указателей-псевдонимов 77
2.9.2 Анализ вызовов виртуальных функций и косвенных вызовов 78
2.9.3 Анализ рекурсивных функций 80
2.10 Методы реализации резюме для различных видов проверок 81
2.10.1 ConstModifedChecker — проверка модификации константных данных 82
2.10.2 IntegerOverfowChecker — проверка на целочисленное переполнение 85
2.10.3 AtomicityChecker — проверка атомарности доступа к разделяемым данным 86
2.10.4 MissingLockChecker — проверка на несериализованный доступ к разделяемой памяти 90
2.10.5 BasicStringBoundChecker — проверка на использование корректного индекса при обращении к элементам строки 92 2.10.6 ThrowWhileCopyChecker — проверка на безопасность обработки исключений в функциях копирования 94
2.10.7 SimpleStreamChecker — проверка операций с файловыми дескрипторами 97
2.11 Построение отчёта о дефекте 100
3 Межмодульный анализ 107
3.1 Реализация межмодульного анализа в статическом анализаторе, использующем для анализа непосредственно исходный код программы 109
3.2 Фаза сборки 110
3.3 Фаза предобработки данных 113
3.4 Фаза анализа. Слияние синтаксических деревьев 114
4 Тестирование разработанного программного комплекса 121
4.1 Выбор тестовых проектов 121
4.2 Методика тестирования 122
4.3 Тестирование покрытия и производительности 124
4.4 Обнаружение дефектов 129
4.5 Общие выводы по результатам тестирования 132
Заключение 139
Список литературы 142
Список рисунков
