--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on July 2010 ---
Boris Hollas wrote: > Hello, > > according to the Jessie tutorial, type invariants are not supported yet. > However, on code using a type invariant I obtained a message to use a > pointer instead. So I changed my type invariant to the one below, which > doesn't produce an error message. Still, I'm unsure whether Jessie uses > this type invariant as I have difficulties proving some related VCs. > > What's the status of type invariants in Boron-20100401 + Jessie? > > typedef struct _Car { > int speed; > }Car; > /*@ type invariant car_speed_constraint(Car* this) = > @ 0 <= this->speed <= 250; > */ > > Hi, The type invariants are one of the features that should be supported soon. For the moment, it is just translated into a predicate declaration, but not inserted automatically at the place it should be. Still, you can manually add some annotations like /*@ requires car_speed_constraint(x) @ ensures car_speed_constraint(x) @*/ ... f(Car *x) { ... } at places you want them used and checked - Claude -- 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 |