A plugin for the Frama-C framework that allows a behavior similar to GCC's -werror option
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.


* About *

framac-werror is a plugin for the C source-code analysis Frama-C platform (www.frama-c.com). It changes the behavior of this tool 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 analyzed 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 guaranty the absence 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 analyzing incomplete applications (in Frama-C's talk) some proof obligations may have a "unknown" state, that is while analyzing 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 plugin to not consider these proofs as erroneous. This is for example useful when checking libraries.

* Where to find it *

framac-werror is hosted on GitHub (www.github.com). This the place to go to get help. 
You are welcome to fill bug and feature reports and contribute code to this project.

This plugin has been written by Sylvain Frédéric Nahas (sylvain DOT nahas AT googlemail DOT com) and is distributed under the LGPL.

* Using it *

After having compiled and installed framac-werror (see the INSTALL file for that), executing
$ frama-c -werror-help
should print the in-line help out. 

The plugin basically adds a new command-line option to Frama-C:
$ frama-c your other options -then -werror

Please note that the "-then" above is important.