Frama-C

Frama-C

Developer(s)	Commissariat à l'Énergie Atomique and Inria
Written in	OCaml
Operating system	Microsoft Windows, Linux, Mac OS X
Available in	English
Type	Formal verification, Static code analysis
License	mostly LGPL, some parts under BSD licenses
Website	frama-c.com

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 and Inria. Frama-C enables the analysis of C programs without executing them.

Architecture

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

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

value analysis: which 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: to verify properties in a deductive manner. Jessie relies on the Why back-end to enable proof obligations to be sent to automatic theorem provers like Z3, Simplify, Alt-Ergo or interactive theorem provers like Coq. Using Jessie, an implementation of bubble-sort or a toy e-voting system can be proved to satisfy their respective specifications.
impact analysis: to highlight in the C source code the impacts of a modification.
slicing: this plugin enables to slice a program (program slicing). It enables to generate a smaller new C program which preserves some given properties^[2].
spare code: this plugin removes useless code from a C program.

Frama-C can be used for the following purposes:

to understand C code which you have not written. In particular Frama-C enables to: observe a set of values, slice the program into shorter programs, navigate in the program.

to prove formal properties on the code. Using specifications written in ANSI/ISO C Specification Language enables to ensure properties of the code for any possible behavior. Frama-C handles floating point numbers ^[3].

to enforce coding standards or code conventions on C source code, by means of custom plugin(s)^[4].

^ Pascal Cuoq et al. "Experience report: OCaml for an industrial-strength static analysis framework". Proceedings of the 14th ACM SIGPLAN international conference on Functional programming. http://portal.acm.org/citation.cfm?id=1596550.1596591.
^ Benjamin Monate, Julien Signoles (2008). "Slicing for Security of Code". Trusted Computing - Challenges and Applications. Lecture Notes in Computer Science. 4968/2008. ISBN 978-3-540-68978-2. http://www.springerlink.com/content/54118148535p1186/.
^ Sylvie Boldo, Thi Minh Tuyen Nguyen (2010). "Hardware-independent proofs of numerical programs". Proceedings of NFM 2010. http://shemesh.larc.nasa.gov/NFM2010/papers/nfm2010_14_23.pdf.
^ David Delmas, Stéphane Duprat, Victoria Moya Lamiel, Julien Signoles. "Taster, a Frama-C plug-in to enforce Coding Standards". Embedded Real Time Software and Systems 2010, Toulouse, France. http://www.erts2010.org/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0003_final.pdf.
^ Jonathan-Christofer Demay, Éric Totel, Frédéric Tronel (2009). "Automatic Software Instrumentation for the Detection of Non-control-data Attacks". Recent Advances in Intrusion Detection. Lecture Notes in Computer Science. 5758/2009. http://www.springerlink.com/content/d5k2p57149065777.