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: dmentre at linux-france.org (David MENTRE)
  • Date: Wed, 7 Dec 2011 15:49:16 +0100
  • In-reply-to: <4EDF792E.3080509@inria.fr>
  • References: <CAC3Lx=aPPQOx6_pVXvyvy2qwCmzTPK8iJpk8rqR05R=Dr7AVbA@mail.gmail.com> <4EDF792E.3080509@inria.fr>
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