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