--- layout: fc_discuss_archives title: Message 21 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 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