--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on July 2012 ---
Hi, thanks for the quick reply. I added: requires \forall unsigned char n,m; 0 <= n < 2 && 0 <= m < 2 ==> \valid(&b.val[n]+m); but it does not changes anything on unsigned char or unsigned int. Arnaud On Jul 6, 2012, at 10:55 AM, Boris Hollas wrote: > On Fri, 2012-07-06 at 10:37 +0200, Arnaud Dieumegard wrote: >> typedef struct{ >> double val[2][2]; >> }t_struct; >> >> t_struct b; >> >> /*@ requires \valid(&b.val); > > Here, you only specify that val[0][0] is valid. See the ACSL doc on how > to specify ranges. > -- > Best regards, > Boris > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss Cordialement, Arnaud Dieumegard PhD Student IRIT-ENSEEIHT / ACADIE 2 rue Charles CAMICHEL BP 7122 31071 TOULOUSE cedex 07 arnaud.dieumegard at enseeiht.fr Tel: 05.34.32.21.64