Почему код недоступен в Frama-C Value Analysis?
При запуске анализа значений Frama-C с некоторыми тестами, например susan в http://www.eecs.umich.edu/mibench/automotive.tar.gzМы заметили, что многие блоки считаются мертвым кодом или недоступны. Однако на практике этот код выполняется, когда мы распечатали некоторую отладочную информацию из этих блоков. Кто-нибудь заметил эту проблему? Как мы можем решить это?
2 ответа
Появления мертвого кода в результатах анализа стоимости Frama-C сводятся к двум аспектам, и даже эти два аспекта являются лишь вопросом человеческих намерений и неразличимы с точки зрения анализатора.
- Реальные ошибки, которые возникают с уверенностью каждый раз, когда достигается конкретное утверждение. Например, код после
y = 0; x = 100 / y;недоступен, потому что программа останавливается на делении каждый раз. Некоторые ошибки, которые должны быть ошибками во время выполнения, не всегда останавливают выполнение, например, запись по неверному адресу. Считай, что тебе повезло, что они делают это в анализе стоимости Frama-C, а не наоборот. - Отсутствие конфигурации контекста анализа, в том числе отсутствие информативной функции main(), которая устанавливает диапазоны вариаций входных данных программы с такими встроенными функциями, как
Frama_C_interval(), отсутствующие библиотечные функции, для которых не указаны ни спецификации, ни код замены, код сборки внутри программы на C, отсутствующая опция-absolute-valid-rangeкогда уместно, ...
У вашего кода есть особенность, которой нет в списке Паскаля, и которая объясняет некоторые части мертвого кода. Довольно много функций объявлены как таковые
f(int x, int y);
Тип возврата полностью отсутствует. Стандарт C указывает, что такие функции должны возвращать intи Frama-C следует этому соглашению. При анализе этих функций это означает, что они никогда ничего не возвращают на некоторых своих путях
Body of function f falls-through. Adding a return statement.
В верхней части оператора return Frama-C также добавляет /*@ assert \false; аннотация, чтобы указать, что пути выполнения функций, которые ничего не возвращают, должны быть мертвым кодом. В вашем коде эта аннотация всегда ложна: эти функции должны возвращать void, и не int, Вы должны исправить свой код с хорошим типом возврата.