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] Frama-C/Jessie: assigning a pointer with a formal parameter (of type pointer)

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;
 > }
 > /*=========================*/