blob: eb0c45a200ffb38c11bee5ba6cb7d2ec68efd48d (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
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
|
