--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on June 2010 ---
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; */ -- Regards, Boris