--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on November 2009 ---
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. 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. Regards, Boris