--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on November 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Documentation of \valid



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