Как избежать обнаружения неинициализированных переменных при использовании анализа воздействия Frama-C

Question

Я обнаружил, что если в программе есть неинициализированное левое значение (например, переменная X), Frama-C утверждает, что X был инициализирован, но затем утверждение получает окончательный статус недействительным. Кажется, что Frama-C останавливает анализ после обнаружения неверного окончательного статуса, так что фактический результат анализа воздействия (затронутые утверждения) является лишь частью идеального результата. Я хочу, чтобы Frama-C продолжила анализ влияния независимо от этих неинициализированных переменных, но я еще не нашла связанных вариантов. Как бороться с этой проблемой?

Answer 1

Вы вызываете неопределенное поведение, как указано в приложении J.2 стандарта ISO C "Значение объекта с автоматической продолжительностью хранения используется, пока оно не определено" (Примечание для языковых юристов: указанное приложение является информативным, и я не удалось отследить эту претензию до нормативных разделов стандарта, по крайней мере, для C11). Плагин EVA, который используется внутри анализа Impact, ограничивается путями выполнения, которые имеют четкое значение в соответствии со стандартом (пресловутые носовые демоны не являются частью абстрактных доменов EVA). Если таких путей нет, абстрактное выполнение действительно остановится. Надлежащим способом решения этой проблемы является обеспечение правильной инициализации локальных переменных анализируемой программы перед обращением.

Обновить

Я забыл упомянуть, что в следующей версии (16 - Sulphur), чья бета-версия доступна по адресу https://github.com/Frama-C/Frama-C-snapshot/wiki/downloads/frama-c-Sulfur-20171101-beta.tar.gz, у EVA есть опция -val-initialized-locals, чья помощь указывает:

Локальные переменные входят в область полностью инициализированной. Полезно только для анализа программ с ошибками по инициализации.