Frama-c
 |
|
| Developer(s) | Commissariat à l'Énergie Atomique (CEA-List) and Inria |
|---|---|
| Written in | OCaml |
| Operating system | Microsoft Windows, FreeBSD, Linux, Mac OS X |
| Available in | English |
| Type | Formal verification, Static code analysis |
| License | mostly LGPL, some parts under BSD licenses |
| Website | frama-c |
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 Commissariat à l'Énergie Atomique et aux Énergies Alternatives (CEA-List) and Inria. Frama-C, as a static analyzer, inspects programs without executing them.
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:
Frama-C can be used for the following purposes:
...
Wikipedia