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] requires on arrays and strct

Hello,

Le ven. 25 sept. 2009 14:15:03 CEST,
Jean Couron <johcrown at gmail.com> a ?crit :

> hello,
> code in e.c is somethng like
>    typedef struct { int a; } A;
>   typedef struct { A * c[10]; } B;
>    typedef struct { B * c[10]; } C;
>   C v;
>   /* one of the 3 contracts below (wth MAXLEN==10)*/
>   void foo(void);
> 
> 3rd attempt below isnt an excepton: shouldit be also recorded as bug in bts?
> 
> > > /*@ requires \valid((v.c+(0 .. MAXLEN-1))->c+(0 .. MAXLEN-1)); */
> > > frama-c  -main f e.c -jessie
> > > e.c:8:[kernel] user error: Error during annotations analysis: expected a
> > > struct with field c

This message is not a bug: the annotation is not correctly typed: 
v.c+(0..MAXLEN-1) represents a set of pointers to the elements of the
array v.c, i.e. a set of pointers to pointers to B.

Your first annotation asserts the validity of the pointers to A
structures, while your second one says that each cell of the c array in
the B structures is valid (which is pretty much the same as
\valid((v.c[0..MAXLEN-1])->c) with your typedefs). They are correctly
typechecked, but the jessie plug-in does not know how to handle them.

-- 
E tutto per oggi, a la prossima volta.
Virgile