Frama-C


Frama-C is a set of interoperable program analyzers for C programs. The name Frama-C stands for Framework for Modular Analysis of C programs. Frama-C has been developed by the French Commissariat à l'Énergie Atomique et aux Énergies Alternatives and Inria. It has also received funding from the Core Infrastructure Initiative. Frama-C, as a static analyzer, inspects programs without executing them. Despite its name, the software is not related to the French project Framasoft.
WWW frama-c.cea.fr

Architecture

Frama-C has a modular plugin architecture comparable to that of Eclipse (software) or GIMP.
Frama-C relies on CIL to generate an abstract syntax tree.
The abstract syntax tree supports annotations written in ANSI/ISO C Specification Language.
Several modules can manipulate the abstract syntax tree to add ANSI/ISO C Specification Language annotations. Among frequently used plugins are:Value analysis – computes a value or a set of possible values for each variable in a program. This plugin uses abstract interpretation techniques and many other plugins make use of its results.Jessie – verifies properties in a deductive manner. Jessie relies on the Why or Why3 back-end to enable proof obligations to be sent to automatic theorem provers like Z3, Simplify, Alt-Ergo or interactive theorem provers like Rocq or Why. Using Jessie, an implementation of bubble-sort or a toy e-voting system can be proved to satisfy their respective specifications. It uses a separation memory model inspired by separation logic.WP – similar to Jessie, verifies properties in a deductive manner. Unlike Jessie, it focuses on parameterization with regards to the memory model. WP is designed to cooperate with other Frama-C plugins such as the value analysis plug-in, unlike Jessie that compiles the C program directly into the Why language. WP can optionally use the Why3 platform to invoke many other automated and interactive provers.E-ACSL – instruments a program to perform runtime verification of properties, possibly in complement with other plugins such as value analysis and WP.Impact analysis – highlights the impacts of a modification in the C source code.Slicing – enables slicing of a program. It enables generation of a smaller new C program that preserves some given properties.Spare code – removes useless code from a C program.
Other plugins are:Dominators – computes dominators and postdominators of statements.From analysis – computes functional dependencies.

Features

Frama-C can be used for the following purposes: