Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000096Frama-CKernelpublic2009-05-25 15:552009-07-03 15:47
Reporterbobot 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFrama-C Beryllium-20090601-beta1Fixed in VersionFrama-C Beryllium-20090601-beta1 
Summary0000096: "logic set<struct something *> f(...)" throw a syntax error
Description============
typedef struct node {
    int hd;
    struct list * next;
} list;

/*@
  logic set<struct node *> tata(struct node * p) = \empty;
  @*/
=============

throw:
File "empty.c", line 7, characters 19-23: syntax error while parsing annotation


However there is a natural work around :
=============
/*@
  logic set<list *> tata(struct node * p) = \empty;
  @*/
=============
is correct.
Additional Informationsvn id : 5303
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-05-25 15:55 bobot New Issue
2009-05-25 16:04 signoles Status new => assigned
2009-05-25 16:04 signoles Assigned To => virgile
2009-06-03 17:46 virgile Target Version => Frama-C Beryllium
2009-06-05 19:17 svn Checkin
2009-06-08 17:05 svn Checkin
2009-06-08 17:05 svn Status assigned => resolved
2009-06-08 17:05 svn 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-07-03 15:47 svn Checkin


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker