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! _______________________________________________ Fedora-ocaml-list mailing list Fedora-ocaml-list@xxxxxxxxxx https://www.redhat.com/mailman/listinfo/fedora-ocaml-list
