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 (CEA-List) 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.

Frama-C has a modular plugin architecture comparable to that of Eclipse (software) or GIMP.

Frama-C relies on CIL (C Intermediate Language) to generate an abstract syntax tree. The abstract syntax tree supports annotations written in ANSI/ISO C Specification Language (ACSL).

Several modules can manipulate the abstract syntax tree to add ANSI/ISO C Specification Language (ACSL) annotations. Among frequently used^[vague] plugins are:

Other plugins are:

Frama-C can be used for the following purposes: