0000096: "logic set<struct something *> f(...)" throw a syntax error

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000096

Frama-C

Kernel

public

2009-05-25 15:55

2009-07-03 15:47

Reporter

bobot

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Frama-C Beryllium-20090601-beta1

Fixed in Version

Frama-C Beryllium-20090601-beta1

Summary

0000096: "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 Information

svn id : 5303

Tags

No 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