Разработчик Cppcheck (Daniel Marjamäki) собирается добавить возможность верификации ПО на C и C++ в свой статический анализатор.

Верификация ПО в Cppcheck

В режиме «верификации» Cppcheck будет выдавать предупреждение, если не удастся подтвердить, что код безопасный, однако это может приводить к шуму (множественным предупреждениям).

Планы реализации

Режим верификации будет реализован последовательно. На первом этапе работа будет сконцентрирована над проверкой «деление на ноль». Это относительно простая проверка. Каждая функция будет проверяться отдельно. При этом предполагается, что все входные данные могут иметь произвольное значение. Проверки других типов неопределённого поведения будут добавлены позже. Также планируется улучшить синтаксический анализ C и C++.

Ускорение разработки

Цель сбора средств на Kickstarter — ускорение разработки режима верификации. Планируется добавить данную возможность в любом случае, но работа может занять больше времени, если средства не будут собраны. Если же средства будут собраны то Даниель сможет взять отпуск на основной работе, чтобы полностью посвятить своё рабочее время проекту cppcheck.

Цели проекта

• Устранение ложноотрицательных срабатываний тестов деления на ноль в Juliet и ITC.

• Исправление ложноположительного срабатывания (см. BUG#9402).

• Улучшение анализатора C++.

>>> Подробности на Kickstarter