2021-01-27 12:00 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000160Frama-CPlug-in > jessiepublic2014-02-12 16:56
Reporterdpariente 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Beryllium-20090601-beta1 
Summary0000160: \at(...,Post) in assigns clause
Description"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
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0000200

signoles (manager)

From a thread initiated by Dillon on Frama-C discuss:
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-June/001260.html
+Notes

-Issue History
Date Modified Username Field Change
2009-06-22 19:54 dpariente New Issue
2009-06-23 08:37 signoles Status new => assigned
2009-06-23 08:37 signoles Assigned To => cmarche
2009-06-23 08:38 signoles Note Added: 0000200
2009-06-23 11:22 cmarche Status assigned => resolved
2009-06-23 11:22 cmarche Resolution open => fixed
2009-06-23 18:02 signoles Status resolved => closed
2009-06-23 18:03 signoles Fixed in Version => Frama-C Beryllium beta-1
2009-06-24 14:48 svn
2009-06-24 14:48 svn Status closed => resolved
2009-06-24 14:49 signoles Status resolved => closed
2013-12-19 01:13 signoles Source_changeset_attached => framac master d6eb6682
2014-02-12 16:56 signoles Source_changeset_attached => framac stable/neon d6eb6682
+Issue History