Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Type invariants

  • Subject: [Frama-c-discuss] Type invariants
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Fri, 09 Jul 2010 10:52:10 +0200
  • In-reply-to: <1277125669.1505.7.camel@iti27>
  • References: <1277125669.1505.7.camel@iti27>
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                    |