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

[Frama-c-discuss] Type invariants



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                    |