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

> 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