|This article needs additional citations for verification. (September 2009)|
|Developer(s)||Commissariat à l'Énergie Atomique and Inria|
|Operating system||Microsoft Windows, FreeBSD, Linux, Mac OS X|
|Type||Formal verification, Static code analysis|
|License||mostly LGPL, some parts under BSD licenses|
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.
- 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 Coq 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 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. Unlike Jessie (which compiles the C program directly into the Why language), WP is designed to cooperate with other Frama-C plugins such as the value analysis plug-in. WP can optionally use the Why3 platform to invoke many other automated and interactive provers.
- 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.
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.
- to instrument C code against some security flaws
- 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.
- "Why homepage".
- 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.
- Sylvie Boldo, Thi Minh Tuyen Nguyen (2010). "Hardware-independent proofs of numerical programs" (PDF). Proceedings of NFM 2010.
- David Delmas, Stéphane Duprat, Victoria Moya Lamiel, Julien Signoles. "Taster, a Frama-C plug-in to enforce Coding Standards" (PDF). Embedded Real Time Software and Systems 2010, Toulouse, France.
- 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.