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: Claude.Marche at inria.fr (Claude Marche)
  • Date: Wed, 07 Dec 2011 15:33:18 +0100
  • In-reply-to: <CAC3Lx=aPPQOx6_pVXvyvy2qwCmzTPK8iJpk8rqR05R=Dr7AVbA@mail.gmail.com>
  • References: <CAC3Lx=aPPQOx6_pVXvyvy2qwCmzTPK8iJpk8rqR05R=Dr7AVbA@mail.gmail.com>
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

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.

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.

- Claude


Asma Tafat, Sylvain Boulm?, and Claude March?. A refinement methodology 
for object-oriented programs. In Bernhard Beckert and Claude March?, 
editors, Formal Verification of Object-Oriented Software, Revised 
Selected Papers Presented at the International Conference, FoVeOOS 2010, 
volume 6528 of Lecture Notes in Computer Science, pages 153-167. 
Springer, January 2011.

Romain Bardou. Verification of Pointer Programs Using Regions and 
Permissions. Th?se de doctorat, Universit? Paris-Sud, 2011. 
http://romain.bardou.fr/thesis/bardou11phd.pdf.

Romain Bardou. Invariants de classe et syst?mes d'ownership. Master's 
thesis, Master Parisien de Recherche en Informatique, 2007. (in french)
http://romain.bardou.fr/papers/stage2007r.pdf