|
Эта публикация цитируется в 2 научных статьях (всего в 2 статьях)
Формализация определения ошибок при статическом символьном выполнении
В. К. Кошелев Институт системного программирования РАН
Аннотация:
Данная работа посвящена формализации понятия ошибочной ситуации при статическом анализе исходного кода, основанном на символьном выполнении. При использовании методов символьного выполнения для статического анализа необходимо пересматривать критерий выдачи ошибок, так как оригинальный критерий приводит к чрезмерному числу ложных срабатываний. Для решения этой проблемы предлагаются альтернативные определения ошибочной ситуации, сообщающие об ошибке только в том случае, когда она происходит на некотором множестве значений входных переменных. Примерами таких множеств являются, например, множество значений входных переменных, при которых управление пройдет через заданную точку программы, или множество значений, при которых управление пройдет по заданному пути в графе потока управления. В данной работе рассматриваются различные способы задания таких множеств начальных значений. Анализируются полученные таким образом определения ошибочных ситуаций. Приводятся алгоритмы, обнаруживающие данные ошибочные ситуации, а также доказывается их соответствие. Рассматривается практическое применение приведённых определений ошибочных ситуаций, а именно: классификация срабатываний инструментов статического анализа; учет неизвестных контракта вызова анализируемой функции; использование определения ошибочной ситуации в качестве запроса к SMT-решателю для поиска точного решения в соответствии с данными определением.
Ключевые слова:
статический анализ, определение ошибочной ситуации, символьное выполнение.
Образец цитирования:
В. К. Кошелев, “Формализация определения ошибок при статическом символьном выполнении”, Труды ИСП РАН, 28:5 (2016), 105–118
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/tisp70 https://www.mathnet.ru/rus/tisp/v28/i5/p105
|
|