--- layout: fc_discuss_archives title: Message 66 from Frama-C-discuss on September 2009 ---
[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