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: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Wed, 07 Dec 2011 14:59:58 +0100
  • In-reply-to: <CAC3Lx=aPPQOx6_pVXvyvy2qwCmzTPK8iJpk8rqR05R=Dr7AVbA@mail.gmail.com>
  • References: <CAC3Lx=aPPQOx6_pVXvyvy2qwCmzTPK8iJpk8rqR05R=Dr7AVbA@mail.gmail.com>
Hello David,

On 12/07/2011 12:24 PM, David MENTRE wrote:
> What is the current status of global variable invariant ("//@ global
> invariant ..." notation) in Frama-C?
>
>  From what I have gathered for Nitrogen release:
>    * ACSL: supported, defined in ACSL documentation;
>
>    * Jessie: Not supported, according to ?5.2.3;
>
>    * WP: Not supported, according to a warning printed on console;
>
>    * Value Analysis: Not supported? (a warning is printed on console
> "warning: ignoring status of global invariant ...")

Actually this warning is emitted by the Frama-C kernel, not by Value 
Analysis. Global invariants are correctly parsed and typed by Frama-C, 
but it is not possible yet to assign them a validity status.

> Is there any plan to support global invariant in future releases[1]?

It could be fully supported by the kernel in Frama-C Oxygen or Frama-C 
Fluorine, but it is not 100% guarantee. For the above plug-ins, I don't 
know what is planned.

> Global invariant seems to me quite important to ensure correctness of
> a software (for safety or security properties).
>
> 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. ;-)

Boris Hollas' workaround is correct for weak invariants but not for 
strong invariant: in this last case, you have to insert a corresponding 
annotation at each sequence point of your program (see ACSL Reference 
Manual, Section 2.11). Definitively cumbersome to do such a task 
manually, but writing a small plug-ins in order to insert these 
annotations should be a not-so-much amount of work.

Best regards,
Julien