--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on December 2011 ---
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