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