--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on November 2009 ---
Hello Boris, > > In this example, Jessie can't verify memory safety: > > typedef int arr3[3]; > > /*@ requires \valid(a); > */ > foo(arr3 a) { > a[2] = 0; > } > > In this case, arr3 is not treated as type of ist own, ie an array of type int[3]. I feel that this is conceptually different to the struct example. The case of function arguments is a bit special: an array is considered as a pointer in this context (ISO norm, 6.7.5.3. The special case of typedef int arr3[static 3] is not accepted by Frama-C at the moment). Thus \valid(a) only implies the validity of an int pointer, and not the validity of a+2... Best regards, -- E tutto per oggi, a la prossima volta. Virgile