--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on November 2009 ---
>>>>> The documentation states "\valid(s) holds if and only if >>>>> dereferencing any p \in s is safe." However, it's not clear what >>>>> dereferencing means wrt structs. >>>>> >>>> If p is a pointer to struct B, >>>> >>>> \valid(p) means that it is safe to do >>>> >>>> struct B s; >>>> s = *p; >>>> >>>> in your program. It's not really different from validity for >>>> a pointer to int or char. >>>> >>> >>> It's not different if we assume that Frama-C treats a struct as a type, ie knows the internal representation of B - in the same way it knows about int and char. >>> >>Which is indeed a valid assumption. Frama-C treats a struct as a type. >>(On the other hand, I agree that the Jessie plugin does not support well >>passing a struct by value.) >>> 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]. >>As said by Virgile, in this context a is indeed of type int* and not >>int[3]. You need to put >> >> requires \valid(a+(0..2)); >>> I feel that this is conceptually different to the struct example. >>> >>Yes: struct are passed by value, i.e copied on the stack, whereas array >>are not, only their address is passed. In the struct example I've give, the struct is also passed by reference: struct A { int x; int y; }; struct B { struct A a; int z; }; /*@ requires \valid(p); */ void foo(struct B *p) { p->a.x = 0; p->z = 0; } My point is that I feel that Jessie treats the types arr3 (array of length 3) and B (struct) differently and that this is not obvious from the ACSL documentation. There are numerous examples how to annotate arrays, but no similar example for a struct. My proposal is to include the struct example in the documentation in 2.3.4 to explain this point. Regards, Boris