--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on November 2009 ---
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 |