Описание тега frama-c

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

Большинство анализов, предоставляемых в Frama-C, являются "надежными": при использовании в пределах ограниченного периметра все поведения, которые могут произойти во время выполнения, включаются в поведения, статически предсказываемые Frama-C. Несмотря на возможность ошибок, плагины должны использоваться в соответствии с документацией, чтобы свойство сохранялось. Это позволяет использовать Frama-C для формальной проверки программ C.

На платформе доступны два плагина, Jessie и Wp, для проверки функциональных свойств. Можно показать, что реализация A C придерживается описания на языке спецификации ACSL того, что программа должна делать.