Goanna. Обнаружитель дефектов на основе modelchecking

Goanna позволяет обнаруживать следующие типы дефектов в программах на С/С++:

• ошибки выхода за границу массива


• арифметические ошибки


• ошибки копирования


• ошибки непредсказуемого поведения (неинициализированные переменные)


• ошибки работы с памятью


• ошибки с указателями на функции


• ошибки неправильного использования указателей


• ошибки неспецифицированного порядка выполнения.

Для обнаружения дефектов используется верификатор NuSMV. Подробнее использование верификатора описано в статье Goanna: Syntactic Software Model Checking

Разработчики проверяли средство на свободно-распространяемых проектах, в том числе на Firefox.Плотность обнаружения дефектов составила 0.3-2 дефекта на 1000 строк исходного кода.

Для получения более объективной картины ниже приведены результаты средства на простых тестах (менее 20 строк кода, 1 функция):

• Выход за границу массива -- находятся случаи, когда реально выходят за границу массива и не находятся случаи, когда выходят за границу размерности (например, a[1][-1] в массиве размера 2x2)


• Разыменование указателя, выведенного за границу объекта -- не обнаруживается вообще


• Переполнения буфера для memcpy не обнаруживается


• Сравнение и вычитание указателей на различные объекты не обнаруживается


• Использование неинициализированной переменной (памяти)




• через указатель не находит


• в виде параметров функции находит


• не находится при копировании неинициализированной памяти с помощью memcpy




• Разыменование неинициализированного указателя -- находится


• Разыменование нулевого указателя -- находится в простых случаях, при использовании результата malloc, но не находится для статического указателя (инициализируется нулем)

Необходимо отметить, что ошибки выхода за границу массива достаточно хорошо обнаруживаются средством в рамках одной функции, но не находятся при межпроцедурном варианте теста.

В средстве реализовано обнаружение множества дефектов, то есть после нахождения одного дефекта анализ продолжается. Например, в коде

#include
int main(void)
{
int *p = NULL;
int *q = NULL;
*p = 0;
*q = 0;
return 0;
}

Обнаруживаются ошибки для обоих указателей, хотя после разыменования p программа упадет.

Средство порадовало отсутствием ложных обнаружений, хотя понятно, что для тестирования использовались простые программы, в которых у качественного анализатора не должно быть ложных обнаружений. Если посмотреть возможности обнаружения дефектов, то они весьма средние. Например, крайне сложные и важные для языка C ошибки выхода за границу объекта не обнаруживаются вообще.
Для тестирования использовалась версия goanna-cmdline-linux-2.1.tgz с интерфейсом командной строки.