Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000160Frama-CPlug-in > jessiepublic2009-06-22 19:542014-02-12 16:56
Reporterdpariente 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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

-  Notes
(0000200)
signoles (manager)
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 [^]

- 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 Checkin
2009-06-24 14:48 svn Status closed => resolved
2009-06-24 14:49 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker