"logic set<struct something *> f(...)" throw a syntax error
ID0000096: This issue was created automatically from Mantis Issue 96. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000096 | Frama-C | Kernel | public | 2009-05-25 | 2009-07-03 |
| Reporter | bobot | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | 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 |
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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information