May 26, 2018
Extensible platform for source-code analysis of C
Frama-C is a suite of tools dedicated to the analysis of the source code of software written in C.
Frama-C gathers several static analysis techniques in a single collaborative framework, which allows static analyzers to build upon the results already computed by other analyzers in the framework, and provides sophisticated tools, such as a slicer and dependency analysis.
Frama-C is closer to heuristic bug-finding tools than it is to software metrics tools, but it has two important differences with the former 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.