---
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?
- Subject: [Frama-c-discuss] Status of global invariant in Jessie, WP and Value Analysis?
- From: dmentre at linux-france.org (David MENTRE)
- Date: Thu, 8 Dec 2011 09:54:28 +0100
- In-reply-to: <4EE07A49.7040707@cea.fr>
- References: <CAC3Lx=aPPQOx6_pVXvyvy2qwCmzTPK8iJpk8rqR05R=Dr7AVbA@mail.gmail.com> <4EDF715E.5010601@cea.fr> <CAC3Lx=Y-vLYLcqaWCBrTnTf10VtqqDORrV9eeXkhqYt-gy+-HA@mail.gmail.com> <4EE07A49.7040707@cea.fr>
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