--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on July 2012 ---
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