[Frama-c-discuss] Frama-C/Jessie: assigning a pointer with a formal parameter (of type pointer)

Pariente Dillon Dillon.Pariente at dassault-aviation.com
Mon Jun 22 16:56:35 CEST 2009


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;
}

/*=========================*/
 
no ATP is able to discharge the first PO, with command-line: frama-c
-jessie-analysis file.c
 
Please confirm if this is a feature (code+this kind of assigns clause)
not yet available in Jessie, and that there is no ... particular
tricking issue!?
If so, I'll add a record into the BTS for traceability.
 
Thanks in advance!
Best regards,
Dillon PARIENTE
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090622/fb23dbc0/attachment.htm 


More information about the Frama-c-discuss mailing list