Frama-C
What is Frama-C ?
Frama-C is a suite of tools dedicated to the analysis of the source code of so are written in C.
Frama-C gathers several static analysis techniques in a single collaborative framework. The collaborative approach of Frama-C allows static analyzers to build upon the results already computed by other analyzers in the framework. Thanks to this approach, Frama-C provides sophisticated tools, such as a slicer and dependency analysis.
Static analysis ?
Static analysis of source code is the science of computing synthetic information about the source code without executing it.
To most programmers, static analysis means measuring the source code with respect to various metrics (examples are the number of comments per line of code and the depth of nested control structures). This kind of syntactic analysis can be implemented in Frama-C but it is not the focus of the project.
Others may be familiar with heuristic bug-finding tools. These tools take more of an in-depth look at the source code and try to pinpoint dangerous constructions and likely bugs (locations in the code where an error might happen at run-time). These heuristic tools do not find all such bugs, and sometimes they alert the user for constructions which are in fact not bugs.
Frama-C is closer to these heuristic tools than it is to software metrics tools, but it has two important differences with them: it aims at being correct, that is, never to remain silent for a location in the source code where an error can happen at run-time. And it allows its user to manipulate functional specifications, and to prove that the source code satisfies these specifications.
You may now want to go on to the description of Frama-C's features, to a page with more details about its modular, extensible architecture, or you may want to see Frama-C in action on an example.
PILAT
What is PILAT ?
PILAT (for Polynomial Invariants by Linear Algebra Tool) is an invariant generator based on the study of matrices. It processes loops with polynomial assignments and linearize them, then searches for left eigenvectors of the resulting matrix. Those vectors expresses invariants of the loop.
Pilat is a plug-in of the Frama-C framework. It is written in Ocaml and it is open source under LGPL licence, you can find it here. If you use OPAM, you can get the latest version with "opam install pilat". We applied our tool to this benchmark on deterministic loops and on non-deterministic loops.
Related publications
-
De Oliveira Steven, Bensalem Saddek and Prevosto Virgile(2017, October)
Synthesizing invariants by solving solvable loops
-
De Oliveira Steven, Bensalem Saddek and Prevosto Virgile (2016, October)
Polynomial invariants by linear algebra
-
De Oliveira Steven, Bensalem Saddek and Prevosto Virgile (2016, June)
Algèbre lineaire pour invariant polynomiaux (slides)
CaFE
What is CaFE ?
CaFE (for Caret Frama-c's Extension) is a model-checker being developped in the Frama-C framework. It is based on the temporal logic CaRet, a temporal logic based on Call and Return properties.
CaFE uses the results of Value , a powerful static analyser in Frama-C, in order to generate a recursive state machine over which it performs a model-checking procedure. It is not open source, but it is described in this french article.
