Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] New plugin werror + list of external plugins in the wiki

  • Subject: [Frama-c-discuss] New plugin werror + list of external plugins in the wiki
  • From: sylvain.nahas at googlemail.com (sylvain nahas)
  • Date: Wed, 15 Feb 2012 14:27:43 +0100
Dear Frama-C users,

1. I have published a new plugin named werror. Here is its description.

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.

It can be found on GitHub at https://github.com/sylvainnahas/framac-werror

Feel free to try it, adopt it, publish bug reports or feature request
or contribute. Even if it is small, it still can be improved!

2. The wiki main page was also expended with a chapter "External
plugins" to references plugins not distributed with Frama-C.
See here: http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:start

If you are publishing a Frama-C plugin and wish to let the world know,
you should add it to the list.

Greetings,
Sylvain