--- layout: fc_discuss_archives title: Message 27 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 Claude,

2011/12/7 Claude Marche <Claude.Marche at inria.fr>:
> In short, there is no plan to support global invariants in the Jessie
> plugin.
>
> Supporting data invariants in their full generality, as the ACSL document
> proposes, is challenging because of possible uncontrolled pointer aliasing
> might unexpectedly break invariants. Spec# ownership, mentioned by Boris
> Hollas, is one possible solution that were proposed in that past.
> Experiments were made with Jessie but were not convincing: heavy annotation
> overhead, and many VCs generated not discharged by automated provers. See
> references below

Argh, too bad! (but I understand the technical issues)

> In a more pragmatic point of view, there are ways to support invariants in a
> not-too-complex way if we impose restrictions on the allowed invariants.
> Typically, one may require that invariants should not include any memory
> dereferencing.

I need to think and look at actual code about it but it could be a
good starting point. I think it would be usable for simple safety
critical programs. But writing C code without using pointers is a
challenge. ;-)

> David, may be you could encourage progress towards the support of invariants
> if you can tell what kind of invariants you have in mind, and in particular
> whether the restriction above would be too much for you or not.

A first example (that would fit your restriction):
"""
int access_count = 0;
int locked = 0;
//@ global invariant access_count > 3 ==> locked == 1;
"""

I'll look at code to give more feedback.

Best regards,
david