This is a list of plug-ins that you may find useful but are not distributed with Frama-C itself. They are not officially supported by the Frama-C developers; to get support, you should contact the original authors through the web site where the source is hosted, or try your luck on the mailing list.
Add your own plug-in if you think it can be useful to other and want to share it with the world!
The Jessie plug-in allows deductive verification of C programs annotated with ACSL. It uses internally the languages and tools of the Why platform. The generated verification conditions can be submitted to external automatic provers such as Simplify, Alt-Ergo, Z3, Yices, CVC3. For more complex situations, interactive theorem provers can be used to establish validity of VCs. Please look at the Jessie web page for more details.
Jessie is one of the oldest plug-ins of Frama-C; some of the questions asked about it have been gathered on their own page, or in the FAQ.
CELIA is a tool for the static analysis and verification of C programs manipulating dynamic (singly linked) lists. The static analyser computes for each control point of a C program the assertions which are true (i.e., invariant) at this control point. These asssertions express properties about the shape of the lists, their size, the relations between the data (or the sum, or the multiset of data) in list cells. The analysis is inter-procedural, i.e., the assertions computed relate the procedure local heap on entry to the corresponding local heap on exit of the procedure. The results of the analysis can provide insights about equivalence of procedures on lists or null pointer dereferencing. The verifier is an experimental feature.
This plug-in changes the behaviour of Frama-C so that it returns a non-null error code to the OS if there are proof obligations that could not be validated.
It is intended to be used in automated settings like Makefiles, when users want confidence they can not overlook a validation error. Build processes may be very long and verbose and by default Frama-C returns an error code of 0 even if the code to be analysed contains run-time errors. The risk that a developer ignores a warning is real. Since the point of using tools like Frama-C is to garanty the abscence of errors altogether, a stricter behavior than the default may be sensible. With the -werror option, building will by interrupted as soon as a problem has been detected.
When analysing incomplete applications (in Frama-C's talk) some proof obligations may have a “unknown” state, that is while analysing the code the tool does not have enough information to decide if these constraints are valid or invalid. The plugin offers command-line arguments that tell the plug-in to not consider these proofs as erroneous. This is useful when checking libraries for example.
This plugin allows to specify for code annotations (spec of blocks) which coq strategy to apply.
Basically, it will update the default strategy before calling WP.
It provides a grammar extension of specification allowing to specify the target tactic.
This plugin, developed by Adelard, provides a simple way to discover potential concurrency problems in interrupt-driven C code, and is intended for use with small embedded systems. It operates without using the value analysis plugin, which makes it fast but unable to analyse pointers. Command-line and GUI versions are available.