Frama-C Bug Tracking System - Frama-C
View Issue Details
0001149Frama-CPlug-in > jessiepublic2012-04-16 10:502013-03-27 09:44
nmuller 
virgile 
normalminoralways
closedfixed 
Frama-C Carbon-20110201 
Frama-C Oxygen-20120901 
0001149: function names are restricted due to exclusion of ACSL keywords
There are names that the functions are not allowed to have as far as those are also ACLS keywords. In the example joined, one function was called "loop" and this clashed with the corresponding ACSL keyword apparently. As soon as we called this function with another name, there was no problem anymore.
Remark : sometimes, the root cause of a rejection in parsing is quiet obscure and not explicit.
No tags attached.
c annot.c (457) 2012-04-16 10:50
https://bts.frama-c.com/file_download.php?file_id=367&type=bug
Issue History
2012-04-16 10:50nmullerNew Issue
2012-04-16 10:50nmullerStatusnew => assigned
2012-04-16 10:50nmullerAssigned To => virgile
2012-04-16 10:50nmullerFile Added: annot.c
2012-04-16 13:14yakobowskiNote Added: 0002878
2012-04-16 13:14yakobowskiStatusassigned => feedback
2012-04-16 13:14yakobowskiAdditional Information Updated
2012-04-16 16:41nmullerNote Added: 0002884
2012-04-16 16:49yakobowskiNote Added: 0002886
2012-04-16 16:49yakobowskiCategoryKernel > ACSL implementation => Plug-in > jessie
2012-04-16 16:49yakobowskiStatusfeedback => assigned
2012-04-16 17:37nmullerNote Added: 0002889
2012-04-16 18:51nmullerNote Added: 0002894
2012-04-17 17:28virgileNote Added: 0002931
2012-04-17 17:28virgileStatusassigned => resolved
2012-04-17 17:28virgileFixed in Version => Frama-C GIT, precise the release id
2012-04-17 17:28virgileResolutionopen => fixed
2013-03-27 09:43signolesNote Added: 0003781
2013-03-27 09:44signolesFixed in VersionFrama-C GIT, precise the release id => Frama-C Oxygen-20120901
2013-03-27 09:44signolesStatusresolved => closed

Notes
(0002878)
yakobowski   
2012-04-16 13:14   
I do not understand what the problem is. This code parses just fine, even with one function called "loop". What did you try exactly? Regarding error messages: we are constrained by the underlying parser generator, in this case Yacc. It is unfortunately customary for errors to be reported on the wrong syntax element, but there is very little we can do.
(0002884)
nmuller   
2012-04-16 16:41   
The file is the one that has been attached. I am not convinced by the argument that, due to the usage of yacc, you couldn't do another way than just give it over in case of function name clash. There are classical examples (in lex and yacc manuals) of how to strip out the differentiate when we are in frama-c annotation and when we are in C... By the way, the error message that we get is just not explicit enough. And we must investigate in the .jc file to understand what happens
(0002886)
yakobowski   
2012-04-16 16:49   
A backtrace would have been quite useful in this example (although, to give you credit, you included one in most of your bugs). The problem here is not in Frama-C, but in Jessie. More precisely, loop is probably a Why keyword, which is why the file generated by Jessie cannot be parsed. I though that problematic names got renamed, but maybe this particular keyword was forgotten.
(0002889)
nmuller   
2012-04-16 17:37   
I would agree with you. The command I tried is just : frama-c -jessie -jessie-atp alt-ergo annot.c If you need additionnal traces, just say me which command needs be done and which file to be retrieved...
(0002894)
nmuller   
2012-04-16 18:51   
Under Nitrogen : frama-c -jessie file.c -> KO frama-c -jessie -jessie-atp file.c -> KO
(0002931)
virgile   
2012-04-17 17:28   
This is indeed an issue of the Jessie plug-in not sanitizing some identifiers considered by Jessie as keywords. Fixed in Jessie svn.
(0003781)
signoles   
2013-03-27 09:43   
Fixed in Frama-C Oxygen + Why 2.32.