2021-03-01 05:08 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000840Frama-CKernelpublic2014-02-12 16:58
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritytextReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • c file icon ftest.c (59 bytes) 2011-05-27 13:26 -
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    //@ assert \result;
    extern int p(void);
    
    c file icon ftest.c (59 bytes) 2011-05-27 13:26 +

-Relationships
+Relationships

-Notes

~0003083

yakobowski (manager)

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)

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)

The issue lies with -pp-annot (set implicitly by Jessie)

~0004643

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