| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000862 | Frama-C | Kernel > ACSL implementation | public | 2011-06-10 10:19 | 2013-06-20 15:18 | ||||
| Reporter | ckunz | ||||||||
| Assigned To | virgile | ||||||||
| Priority | normal | Severity | tweak | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Carbon-20110201 | ||||||||
| Target Version | Fixed in Version | Frama-C Fluorine-20130401 | |||||||
| Summary | 0000862: ACSL parser + pretty-printer | ||||||||
| Description | Logic assertions of the form (a) //@ assert x == y^z; are parsed as (x==y)^y and are thus rejected by the type-checker. One must instead write the assertion above as follows (b) //@ assert x == (y^z); This may be understandable. The pretty-printer, however, after parsing the term (b), outputs the term (a), making the output of the pretty-printer a program that is syntactically invalid. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
signoles (manager) 2013-06-20 15:18 |
Don't know exactly in which version this bug was fixed, but it does not appear anymore in Frama-C Fluorine. The second form is correct and correctly outputs by the pretty-printer. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2011-06-10 10:19 | ckunz | New Issue | |
| 2011-06-10 10:19 | ckunz | Status | new => assigned |
| 2011-06-10 10:19 | ckunz | Assigned To | => virgile |
| 2013-06-20 15:18 | signoles | Note Added: 0003976 | |
| 2013-06-20 15:18 | signoles | Status | assigned => closed |
| 2013-06-20 15:18 | signoles | Resolution | open => fixed |
| 2013-06-20 15:18 | signoles | Fixed in Version | => Frama-C Fluorine-20130401 |
| Issue History |