| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000840 | Frama-C | Kernel | public | 2011-05-27 13:26 | 2014-02-12 16:58 | ||||
| Reporter | Jochen | ||||||||
| Assigned To | virgile | ||||||||
| Priority | normal | Severity | text | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Carbon-20110201 | ||||||||
| Target Version | Fixed in Version | Frama-C Oxygen-20120901 | |||||||
| Summary | 0000840: syntax error message refers to (true error line + 5 lines) | ||||||||
| Description | In the attached program, I confused "ensures" and "assert" in the contract of p() in line 20. However, the syntax error message refers to 5 lines below (i.e. line 25). If the error is moved e.g. to line 10 the message refers to line 15. Usually there is other C- or Acsl-code after the error; the message is rather confusing in that cases. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
yakobowski (manager) 2012-06-09 23:59 |
I cannot reproduce the issue: the error is reported at line 21, including with Carbon. If you still notice a problem, can you also supply your OCaml version? |
|
Jochen (reporter) 2012-06-10 10:42 |
Trying to reproduce the behavior with "frama-c ftest.c", I got the error report referring to line 21, as you did. However, trying "frama-c -jessie ftest.c", I still get it at line 25. "frama-c -wp ftest.c" reports at line 21 again. My frama-c version just employed is Nitrogen-20111001. My ocaml version is reported as 3.12.1 by the command "ocaml -version". |
|
virgile (developer) 2012-07-02 11:20 |
The issue lies with -pp-annot (set implicitly by Jessie) |
|
2014-02-12 16:58 |
Fix committed to stable/neon branch. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2011-05-27 13:26 | Jochen | New Issue | |
| 2011-05-27 13:26 | Jochen | File Added: ftest.c | |
| 2011-05-27 13:49 | signoles | Status | new => assigned |
| 2011-05-27 13:49 | signoles | Assigned To | => virgile |
| 2012-06-09 23:59 | yakobowski | Note Added: 0003083 | |
| 2012-06-09 23:59 | yakobowski | Status | assigned => feedback |
| 2012-06-10 10:42 | Jochen | Note Added: 0003086 | |
| 2012-07-02 11:20 | virgile | Note Added: 0003210 | |
| 2012-07-02 11:20 | virgile | Status | feedback => acknowledged |
| 2012-07-03 10:40 | svn | ||
| 2012-07-03 10:40 | svn | Status | acknowledged => resolved |
| 2012-07-03 10:40 | svn | Resolution | open => fixed |
| 2012-07-03 17:45 | svn | ||
| 2012-09-19 17:15 | signoles | Fixed in Version | => Frama-C Oxygen-20120901 |
| 2012-09-19 17:16 | signoles | Status | resolved => closed |
| 2013-12-19 01:11 | Source_changeset_attached | => framac master b6f293ba | |
| 2013-12-19 01:11 | Source_changeset_attached | => framac master 27ba5dc5 | |
| 2014-02-12 16:54 | Source_changeset_attached | => framac stable/neon b6f293ba | |
| 2014-02-12 16:54 | Source_changeset_attached | => framac stable/neon 27ba5dc5 | |
| 2014-02-12 16:58 | Note Added: 0004643 | ||
| 2014-02-12 16:58 | Status | closed => resolved | |
| Issue History |