--- layout: fc_discuss_archives title: Message 40 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:
> 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.
>   
Of course we will be glad to enhance the documentation, but yet I don't 
understand exactly where is the misunderstanding.

Beware that there is ACSL, which is a specification language documented 
in the ACSL document, then there is the Frama-C implementation which 
partially implements ACSL, and then there is Jessie which is a Frama-C 
plugin, which tries to do is best to verify that C code satisfy its ACSL 
annotations. On the example above, Jessie is happy, which seems to be 
right to me: as soon as p points to a properly allocated memory block of 
type B, then both
p->a.x and p->z are safe dereferencing.

I know that there are cases not very different where Jessie does not 
verify corret annotations, e.g. BTS #102. But this does not seem to be 
your point: is it ? In that case please send an example which 
illustrates the point.

And again, why do you say Jessie treats type arr3 differently from B: 
Jessie just tries to model the semantics of C: struct are passed by 
value whereas arrays are never passed by value.

- Claude

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