2021-03-01 05:11 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001149Frama-CPlug-in > jessiepublic2013-03-27 09:44
Assigned Tovirgile 
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001149: function names are restricted due to exclusion of ACSL keywords
DescriptionThere 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 InformationRemark : sometimes, the root cause of a rejection in parsing is quiet obscure and not explicit.
TagsNo tags attached.
Attached Files
  • c file icon annot.c (457 bytes) 2012-04-16 10:50 -
    /* run.config
      OPT: -fct-pdg f1 -main f1 -journal-disable
      OPT: -fct-pdg loop -main loop -journal-disable
    int G;
    int f1 (int x) {
      int a = 10;
        if (x < 10)
          x = 10;
    L : x++;
        //@ assert x > G+a ;
        x = 3;
        // @ assert x < \at(x,L) ; TODO : \at not implemented yet
        return x;
    int loop (int n) {
      int i, s = 0;
      /*@ loop invariant 0 <= i <= n ;
        @ loop variant n-i;
      for (i = 0; i < n; i++)
        s += 2;
      return s;
    c file icon annot.c (457 bytes) 2012-04-16 10:50 +




yakobowski (manager)

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.


nmuller (reporter)

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


yakobowski (manager)

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.


nmuller (reporter)

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...


nmuller (reporter)

Under Nitrogen :
frama-c -jessie file.c -> KO
frama-c -jessie -jessie-atp file.c -> KO


virgile (developer)

This is indeed an issue of the Jessie plug-in not sanitizing some identifiers considered by Jessie as keywords. Fixed in Jessie svn.


signoles (manager)

Fixed in Frama-C Oxygen + Why 2.32.

-Issue History
Date Modified Username Field Change
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
+Issue History