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
- Subject: [Frama-c-discuss] Documentation of \valid
- From: Claude.Marche at inria.fr (Claude Marche)
- Date: Mon, 16 Nov 2009 11:15:57 +0100
- In-reply-to: <FC0686BB6178BC43B9DC035287A11A720DBD5C06AF@SI-MBX12.de.bosch.com>
- References: <FC0686BB6178BC43B9DC035287A11A720DBD57FB8C@SI-MBX12.de.bosch.com> <A4D9A80C-4F63-4879-9B09-D22780EFCF8D@cea.fr> <FC0686BB6178BC43B9DC035287A11A720DBD57FBC9@SI-MBX12.de.bosch.com> <4AFD151D.7090600@inria.fr> <FC0686BB6178BC43B9DC035287A11A720DBD5C06AF@SI-MBX12.de.bosch.com>
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 |
- Follow-Ups:
- [Frama-c-discuss] Documentation of \valid
- From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
- [Frama-c-discuss] Documentation of \valid
- References:
- [Frama-c-discuss] Documentation of \valid
- From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
- [Frama-c-discuss] Documentation of \valid
- From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
- [Frama-c-discuss] Documentation of \valid
- From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
- [Frama-c-discuss] Documentation of \valid
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] Documentation of \valid
- From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
- [Frama-c-discuss] Documentation of \valid
- Prev by Date: [Frama-c-discuss] Documentation of \valid
- Next by Date: [Frama-c-discuss] [Jessie Plugin] Can we trust prover CVC3 version 2.1 ?
- Previous by thread: [Frama-c-discuss] Documentation of \valid
- Next by thread: [Frama-c-discuss] Documentation of \valid
- Index(es):