Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0000840Frama-CKernelpublic2011-05-27 13:262014-02-12 16:58
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritytextReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0000840: syntax error message refers to (true error line + 5 lines)
DescriptionIn 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.
TagsNo tags attached.
Relationships
Attached Filesc ftest.c (59) 2011-05-27 13:26
https://bts.frama-c.com/file_download.php?file_id=224&type=bug

Notes
(0003083)
yakobowski   
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?
(0003086)
Jochen   
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".
(0003210)
virgile   
2012-07-02 11:20   
The issue lies with -pp-annot (set implicitly by Jessie)
(0004643)
   
2014-02-12 16:58   
Fix committed to stable/neon branch.

Issue History
Date ModifiedUsernameFieldChange
2011-05-27 13:26JochenNew Issue
2011-05-27 13:26JochenFile Added: ftest.c
2011-05-27 13:49signolesStatusnew => assigned
2011-05-27 13:49signolesAssigned To => virgile
2012-06-09 23:59yakobowskiNote Added: 0003083
2012-06-09 23:59yakobowskiStatusassigned => feedback
2012-06-10 10:42JochenNote Added: 0003086
2012-07-02 11:20virgileNote Added: 0003210
2012-07-02 11:20virgileStatusfeedback => acknowledged
2012-07-03 10:40svn
2012-07-03 10:40svnStatusacknowledged => resolved
2012-07-03 10:40svnResolutionopen => fixed
2012-07-03 17:45svn
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2013-12-19 01:11Source_changeset_attached => framac master b6f293ba
2013-12-19 01:11Source_changeset_attached => framac master 27ba5dc5
2014-02-12 16:54Source_changeset_attached => framac stable/neon b6f293ba
2014-02-12 16:54Source_changeset_attached => framac stable/neon 27ba5dc5
2014-02-12 16:58Note Added: 0004643
2014-02-12 16:58Statusclosed => resolved