Libre Ocaml formal C verifier
Frama-C[1] stands forFramework for Modular Analysis ofC programs. Frama-C is a set of interoperableprogram analyzers forC programs. Frama-C has been developed by the FrenchCommissariat à l'Énergie Atomique et aux Énergies Alternatives (CEA-List)[2] andInria. It has also received funding from theCore Infrastructure Initiative. Frama-C, as astatic analyzer, inspects programs without executing them. Despite its name, the software is not related to the French projectFramasoft.
| This section is missing information about use of Clang for C++ input at least since 2014. Please expand the section to include this information. Further details may exist on thetalk page.(September 2021) |
Frama-C has a modular plugin architecture[3] comparable to that ofEclipse (software) orGIMP.
Frama-C relies on CIL (C Intermediate Language) to generate anabstract syntax tree.Theabstract syntax tree supports annotations written inANSI/ISO C Specification Language (ACSL).
Several modules can manipulate theabstract syntax tree to addANSI/ISO C Specification Language (ACSL) annotations. Among frequently used[vague] plugins are:
- Value analysis – computes a value or a set of possible values for each variable in a program. This plugin usesabstract 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 toautomatic theorem provers like Z3, Simplify,Alt-Ergo orinteractive theorem provers likeCoq 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 byseparation logic.
- WP (Weakest Precondition) – similar toJessie, 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.
- E-ACSL – (forExecutable ACSL) instruments a program to performruntime verification of properties, possibly in complement with other plugins such as value analysis and WP (e.g. by checking assertions at runtime for the properties that could not be statically verified with the other plugins).
- Impact analysis – highlights the impacts of a modification in the C source code.
- Slicing – enablesslicing 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 inANSI/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 orcode conventions on C source code, by means of custom plugin(s)[7]
- To instrument C code against some security flaws[8]
Book
Category:Family:ML