--- layout: fc_discuss_archives title: Message 36 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 Virgile,

2011/12/8 Virgile Prevosto <virgile.prevosto at cea.fr>:
> This idea (which is not unlike the expose method described by Boris Hollas)
> would be to use a ghost boolean (Yes, I know, support of ghost code should
> be improved too) that would control where the invariant can be broken.

Thank you Boris and Virgile for the feedback, that's interesting!

Best regards,
david