--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on January 2011 ---
Hello, Type invariants are not supported by Jessie for the moment. Moreover, the current distributed version of jessie within Why 2.xx is in a frozen state: no new features will be added anymore in it, instead there is a plan to develop a successor on top of the new Why3 engine whose first public release appeared last december. But I cannot announce any date for availability of it yet. Indeed, there are on-going Ph.D. theses in the ProVal team of INRIA Saclay on the support of data invariants. If you want to know more details about why this support in difficult, I recommend to read the following paper: http://research.microsoft.com/en-us/um/people/leino/papers/krml161.pdf. Although it is centered to OO programming, most of the challenges listed also apply to C. I also recommend the paper http://research.microsoft.com/en-us/um/people/leino/papers/krml209.pdf which gives simple examples of programs for which type invariants are needed but are hard to handle. Finally, notice that a standard workaround for the lack of type invariants is to declare the expected invariant as a predicate, and add this predicate wherever you want it, e.g in pre and/or post-conditions. - Claude On 01/10/2011 09:17 AM, Boris Hollas wrote: > Hello, > > are type invariants supported by the upcoming or current releases of > Jessie or WP? Can specifications for type invariants be used with option > -jessie-infer-annot if APRON is used? > > Regards, > Boris Hollas > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |