--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on December 2011 ---
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>