16 lines
817 B
Text
16 lines
817 B
Text
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.
|
|
|
|
WWW: http://frama-c.com/index.html
|