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



>>>>> 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.

In the struct example I've give, the struct is also passed by reference:

struct A {
    int x;
    int y;
};
struct B {
    struct A a;
    int z;
};

/*@ requires \valid(p);
 */
void foo(struct B *p) {
  p->a.x = 0;
  p->z = 0;
}

My point is that I feel that Jessie treats the types arr3 (array of length 3) and B (struct) differently and that this is not obvious from the ACSL documentation. There are numerous examples how to annotate arrays, but no similar example for a struct. My proposal is to include the struct example in the documentation in 2.3.4 to explain this point.

Regards,
Boris