--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on June 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Type invariants



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