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



Hollas Boris (CR/AEY1) wrote:
> 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.
>   
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.
> Regards,
> Boris
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>   


-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |