Многоуровневый статический анализ исходного кода программ для обеспечения качества программстатья
Статья опубликована в журнале из списка RSCI Web of Science
Статья опубликована в журнале из перечня ВАК
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 24 января 2020 г.
Аннотация:В настоящей статье обсуждаются методы анализа программ для поиска ошибок в исходном коде, которые вместе формируют многоуровневую систему анализа. Первый уровень анализа заключается в проверках по абстрактному синтаксическому дереву и внутрипроцедурном анализе потока данных, а также строит модель памяти программы для последующих уровней, для которой оцениваются значения целочисленных выражений и множества потенциальных целей указателей. Второй уровень -это межпроцедурный анализ на основе аннотаций функции, в котором интересующие свойства программы формулируются как свойства классов значений, выделенных в программе. Наконец, третий уровень анализа - это чувствительный к путям анализ, строящий формулы достижимости точек программы и отслеживающий предикаты, при которых выполняются нужные свойства, а ошибки ищутся с помощью проверки на совместность указанных формул SMT-решателем. Все упомянутые уровни анализа реализованы в инструменте Svace, который демонстрирует масштабируемость анализа до миллионов строк кода и точность в 60-90% истинных срабатываний.