Libre Ocaml formal C verifier
Frama-C stands for "Framework for Modular Analysis of C programs". Frama-C is a set of interoperable program analyzers for 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.
Architecture.
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 plugins are:
Other plugins are:
Features.
Frama-C can be used for the following purposes:
References.
 ;templatestyles src="Reflist/styles.css" / ;