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 |
|
![]() |
||||||
|
![]() |
|
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). |
![]() |
|||
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 |