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