[Svace] Обнаружение ошибок доступа к буферу в программах на языке C/C++ с помощью статического анализа
2016+. И. Дудина. Ещё не опубликована. См. Svace.
2 Есть методы обнаружения последовательности точек программы, прохождение по которым неминуемо приведёт к ошибке. Интересно. 3 Буферы имеют константный размер (известный на момент компиляции), контракт не может запрещать пути, каждая функция считается точкой входа. 4 Ошибка межпроцедурная, если минимальный набор рёбер, приводящий к ней проходит более чем через одну функцию. 5 Ядро Svace проводит статическое символьное исполнение с объединением состояний.
[В примере 1 не закрыта скобка у функции findIdx]
14 pages
Sergey Vartanov, 2007–2020