--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on November 2009 ---
Hollas Boris (CR/AEY1) wrote: > Hello, > > >>> 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. > 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 > -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |