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

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