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] Status of global invariant in Jessie, WP and Value Analysis?

  • Subject: [Frama-c-discuss] Status of global invariant in Jessie, WP and Value Analysis?
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Wed, 07 Dec 2011 12:40:29 +0100
  • In-reply-to: <CAC3Lx=aPPQOx6_pVXvyvy2qwCmzTPK8iJpk8rqR05R=Dr7AVbA@mail.gmail.com>
  • References: <CAC3Lx=aPPQOx6_pVXvyvy2qwCmzTPK8iJpk8rqR05R=Dr7AVbA@mail.gmail.com>
On Wed, 2011-12-07 at 12:24 +0100, David MENTRE wrote:

> What are current work-arounds with Nitrogen? The only possibility I
> can think of is to #define the property and add it as pre- and
> post-conditions to all the functions of a module (with appropriate
> option to preprocess annotations). Cumbersome to say the least. ;-)


As far as I know, different concepts for invariants are being
investigated. The workaround I use is to define a predicate for the
invariant, to #define this as pre- and postcondition and include it in
the contract of each function.
However, you might write a parser or even a plugin that introduces these
annotations automatically (similar to Havoc).
-- 
Best regards,
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111207/23e9e50c/attachment.htm>