--- layout: fc_discuss_archives title: Message 31 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. Pascal