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



Hello Boris,

2011/12/7 Boris Hollas <hollas at informatik.htw-dresden.de>
> As far as I know, different concepts for invariants are being investigated.

Which kind of concepts?

> 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).

OK, thank you for the feedback and suggestion.

Best regards,
david