--- layout: fc_discuss_archives title: Message 70 from Frama-C-discuss on June 2009 ---
Indeed a surprising example, but it can be explained after all. Let me recall the semantics of assigns clauses from the ACSL document: assigns L means that any memory location that is allocated in the pre-state and that do not belong to the set L remains unchanged. Thus: since &x is not allocated in the pre-state, this function only modifies *one* memory location of the pre-state, that is p->rc, then any assigns clause containing at least p->rc is correct. You can try just the clause assigns p->rc; and it is proven valid too. Please try to think about assigns clause from the client's point of view: if any code calls main1(p,r) then it can only observe the side effect on p->rc, and not on *(p->rc) which is not an allocated memory location. - Claude Dillon Pariente wrote: > Thank you Claude for your answer! > > (Indeed, assigns state was different with Caduceus => my old > non-regression examples have to be deeply revisited!) > > Now, BTS is enriched with \at(...,Post) support demand. > > By the way, would you mind explaining why the following annotated code > POs are fully discharged? > The difference with the previous one is that a *dangling* pointer is > used instead of the second parameter. > > /*=========================*/ > typedef struct { int * rc; } S; > > /*@ > requires \valid(p) > && \valid(p->rc) > && \valid(r); > assigns *p->rc,p->rc; > */ > int main1( S* p,int* r) > { int x; > p->rc = &x; > *(p->rc) = 55; > return 1; > } > /*=========================*/ > /* > frama-c -jessie-analysis <file>.c > */ > > Thanks in advance for your comments! > Dillon > >> The first VC is not proved because it is wrong: assigns clause are >> evaluated in the pre-state by default, so assigns *(p->rc) means that >> the cell pointed by p->rc IN THE PRE_STATE is modified. >> >> You should use >> >> assigns *\at(p->rc,Post), p->rc >> >> However, I just checked and the Post label is not yet well handled by >> Jessie. It can be probably solved easily... >> >> So, if you want to fill a bug report, fill it by asking for a full >> support by the Post label in jessie... >> >> >> - Claude >> Pariente Dillon wrote: > > Hello, > > > > (The following issue was discussed earlier with some of you, but I > don't think it is resolved nor recorded into the BTS) > > > > In the following annotated code: > > > > /*=========================*/ > > typedef struct { int * rc; } S; > > > > /*@ > > requires \valid(p) > > && \valid(p->rc) > > && \valid(r); > > assigns *(p->rc),p->rc; > > */ > > int main1( S* p,int* r) > > { > > p->rc = r; > > *(p->rc) = 55; > > return 1; > > } > > /*=========================*/ > > > > _______________________________________________ > 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 |