| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 0000079 | Frama-C | Kernel > ACSL implementation | public | 2009-05-11 16:23 | 2010-02-05 09:44 | ||||||||
| Reporter | boris | ||||||||||||
| Assigned To | virgile | ||||||||||||
| Priority | normal | Severity | feature | Reproducibility | always | ||||||||
| Status | assigned | Resolution | open | ||||||||||
| Product Version | Frama-C Lithium-20081201 | ||||||||||||
| Target Version | Fixed in Version | ||||||||||||
| Summary | 0000079: Better support of //@ style | ||||||||||||
| Description | Annotation consisting of several //@ lines should be supported. Eg, the following code produces a syntax error, whereas the /*@ ... */ style works: //@ loop invariant a[0] == 1; //@ loop invariant 1 <= i; for(i=1; i<10; i++) | ||||||||||||
| Tags | No tags attached. | ||||||||||||
| Attached Files |
| ||||||||||||
 Relationships |
||||||
|
||||||
 Relationships |
| Notes |
|
|
monate (reporter) 2009-05-11 19:59 |
This is conformant with ACSL grammar for loop annotations. Only one special comment is attached to the following loop. /*@ loop invariant a[0] == 1; */ /*@ loop invariant 1 <= i; */ for(i=1; i<10; i++) is also incorrect. |
|
dwheeler (reporter) 2010-01-04 17:41 |
I agree with this proposal. If this isn't done, at *least* provide much clearer error reports. Currently, given two lines of the form: //@ ... //@ ... The system error messages point to lines FAR further down, making debugging the REAL problem very difficult (due to the terribly misleading reference). |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2009-05-11 16:23 | boris | New Issue | |
| 2009-05-11 19:59 | monate | Note Added: 0000052 | |
| 2009-05-15 11:09 | monate | Status | new => assigned |
| 2009-05-15 11:09 | monate | Assigned To | => virgile |
| 2009-06-17 13:38 | signoles | Category | plug-in > jessie => kernel |
| 2010-01-04 17:41 | dwheeler | Note Added: 0000614 | |
| 2010-01-05 08:41 | signoles | Relationship added | related to 0000365 |
| 2010-02-05 09:44 | signoles | Category | Kernel => Kernel > ACSL implementation |
| Issue History |