Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
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.
Attached Filesc file icon ftest.c [^] (59 bytes) 2011-05-27 13:26 [Show Content]

- Relationships

-  Notes
(0003083)
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?
(0003086)
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".
(0003210)
virgile (developer)
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 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 Checkin
2012-07-03 10:40 svn Status acknowledged => resolved
2012-07-03 10:40 svn Resolution open => fixed
2012-07-03 17:45 svn Checkin
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2014-02-12 16:58 Note Added: 0004643
2014-02-12 16:58 Status closed => resolved

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker