Does anybody plan to package Frama-C?
Peter Lemenkov
lemenkov at gmail.com
Wed Jun 4 08:20:21 UTC 2008
I just found it and it looks pretty useful:
http://frama-c.cea.fr/what_is.html
>From the README:
Frama-C is a suite of tools dedicated to the analysis of the source
code of software written in C.
...
If you have a C program and need to
* validate it formally
* look for potential runtime errors
* audit or review it
* reverse engineer it to understand its structure
* generate formal documentation
One or more of the following Frama-C tools may be of assistance to you:
* A parser, a type checker and source level linker for C code
optionally annotated with ACSL formulas.
* A set of builtin static analysis plugins:
o A runtime error detection plug-in based on abstract
interpretation techniques
o A dependencies computation plug-in
o An interactive value analysis plug-in
o A Use/Defs computation plug-in
o A slicing plug-in
o A weakest precondition calculus plug-in based on Floyd-Hoare logic
--
With best regards!
More information about the Fedora-ocaml-list
mailing list