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)

  • Subject: [Frama-c-discuss] Frama-C/Jessie: assigning a pointer with a formal parameter (of type pointer)
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
  • Date: Mon, 22 Jun 2009 16:56:35 +0200
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