Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

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