|Anonymous | Login | Signup for a new account||2019-04-20 11:18 CEST|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0001149||Frama-C||Plug-in > jessie||public||2012-04-16 10:50||2013-03-27 09:44|
|Product Version||Frama-C Carbon-20110201|
|Target Version||Fixed in Version||Frama-C Oxygen-20120901|
|Summary||0001149: function names are restricted due to exclusion of ACSL keywords|
|Description||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.
|Additional Information||Remark : sometimes, the root cause of a rejection in parsing is quiet obscure and not explicit.|
|Tags||No tags attached.|
|Attached Files||annot.c [^] (457 bytes) 2012-04-16 10:50 [Show Content]|
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.
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
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.
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...
Under Nitrogen :
frama-c -jessie file.c -> KO
frama-c -jessie -jessie-atp file.c -> KO
|This is indeed an issue of the Jessie plug-in not sanitizing some identifiers considered by Jessie as keywords. Fixed in Jessie svn.|
|Fixed in Frama-C Oxygen + Why 2.32.|
|2012-04-16 10:50||nmuller||New Issue|
|2012-04-16 10:50||nmuller||Status||new => assigned|
|2012-04-16 10:50||nmuller||Assigned To||=> virgile|
|2012-04-16 10:50||nmuller||File Added: annot.c|
|2012-04-16 13:14||yakobowski||Note Added: 0002878|
|2012-04-16 13:14||yakobowski||Status||assigned => feedback|
|2012-04-16 13:14||yakobowski||Additional Information Updated|
|2012-04-16 16:41||nmuller||Note Added: 0002884|
|2012-04-16 16:49||yakobowski||Note Added: 0002886|
|2012-04-16 16:49||yakobowski||Category||Kernel > ACSL implementation => Plug-in > jessie|
|2012-04-16 16:49||yakobowski||Status||feedback => assigned|
|2012-04-16 17:37||nmuller||Note Added: 0002889|
|2012-04-16 18:51||nmuller||Note Added: 0002894|
|2012-04-17 17:28||virgile||Note Added: 0002931|
|2012-04-17 17:28||virgile||Status||assigned => resolved|
|2012-04-17 17:28||virgile||Fixed in Version||=> Frama-C GIT, precise the release id|
|2012-04-17 17:28||virgile||Resolution||open => fixed|
|2013-03-27 09:43||signoles||Note Added: 0003781|
|2013-03-27 09:44||signoles||Fixed in Version||Frama-C GIT, precise the release id => Frama-C Oxygen-20120901|
|2013-03-27 09:44||signoles||Status||resolved => closed|
|Copyright © 2000 - 2019 MantisBT Team|