Frama-C Bug Tracking System - Frama-C
View Issue Details
0000160Frama-CPlug-in > jessiepublic2009-06-22 19:542014-02-12 16:56
dpariente 
cmarche 
normalminoralways
closedfixed 
 
Frama-C Beryllium-20090601-beta1 
0000160: \at(...,Post) in assigns clause
"at"'s labels support in assigns clause is needed in Jessie to be able to discharge all behavioral POs from the following annotated test code:

typedef struct { int * rc; } S;

/*@ requires \valid(p) && \valid(p->rc) && \valid(r);
    assigns *\at(p->rc,Post),p->rc; */
int main1( S* p,int* r)
{p->rc = r;
 *(p->rc) = 55;
 return 1;
}

//Command-line: frama-c -jessie-analysis e28.c
No tags attached.
Issue History
2009-06-22 19:54dparienteNew Issue
2009-06-23 08:37signolesStatusnew => assigned
2009-06-23 08:37signolesAssigned To => cmarche
2009-06-23 08:38signolesNote Added: 0000200
2009-06-23 11:22cmarcheStatusassigned => resolved
2009-06-23 11:22cmarcheResolutionopen => fixed
2009-06-23 18:02signolesStatusresolved => closed
2009-06-23 18:03signolesFixed in Version => Frama-C Beryllium beta-1
2009-06-24 14:48svnCheckin
2009-06-24 14:48svnStatusclosed => resolved
2009-06-24 14:49signolesStatusresolved => closed

Notes
(0000200)
signoles   
2009-06-23 08:38   
From a thread initiated by Dillon on Frama-C discuss:
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-June/001260.html [^]