--- layout: fc_discuss_archives title: Message 69 from Frama-C-discuss on June 2009 ---
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; > } > /*=========================*/