Frama-C Explained

Frama-C
Developer:	Commissariat à l'Énergie Atomique (CEA-List) and Inria
Programming Language:	OCaml
Operating System:	Microsoft Windows, FreeBSD, OpenBSD, Linux, Mac OS X
Language:	English
Genre:	Formal verification, Static code analysis
License:	mostly LGPL, some parts under BSD licenses

Frama-C^[1] 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 (CEA-List)^[2] 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^[3] 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:

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^[4] 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 a separation memory model inspired by separation logic.
WP (Weakest Precondition) similar to Jessie, verifies properties in a deductive manner. Unlike Jessie, it focuses on parameterization with regards to the memory model. WP is designed to cooperate with other Frama-C plugins such as the value analysis plug-in, unlike Jessie that compiles the C program directly into the Why language. 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.^[5]
Spare code removes useless code from a C program.

Other plugins are:

Frama-C can be used for the following purposes:

To understand C code which you have not written. In particular, Frama-C enables one to observe a set of values, slice the program into shorter programs, and navigate in the program.
To prove formal properties on the code. Using specifications written in ANSI/ISO C Specification Language enables it to ensure properties of the code for any possible behavior. Frama-C handles floating point numbers.^[6]
To enforce coding standards or code conventions on C source code, by means of custom plugin(s)^[7]
To instrument C code against some security flaws^[8]

Web site: Frama-C. frama-c.com. 2016-11-05.
Web site: CEA LIST, Smart digital systems. CEA LIST. 2016-11-05.
Pascal Cuoq. ACM SIGPLAN Notices . Experience report: OCaml for an industrial-strength static analysis framework. 44. 9. 281–286. etal. 10.1145/1631687.1596591. August 2009.
Web site: Why homepage.
Book: Benjamin Monate . Julien Signoles . Slicing for Security of Code . Trusted Computing - Challenges and Applications. Lecture Notes in Computer Science . 2008. 4968/2008. 133–142 . 10.1007/978-3-540-68979-9_10 . 978-3-540-68978-2 .
Sylvie Boldo. Sylvie Boldo . Thi Minh Tuyen Nguyen . Hardware-independent proofs of numerical programs. Proceedings of NFM 2010. 2010.
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.
Book: Jonathan-Christofer Demay . Éric Totel . Frédéric Tronel . Automatic Software Instrumentation for the Detection of Non-control-data Attacks. Recent Advances in Intrusion Detection . Lecture Notes in Computer Science . 2009. 5758/2009. 348–349 . 10.1007/978-3-642-04342-0_19 . 978-3-642-04341-3 .