2021-03-03 03:58 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001553Frama-CKernel > ACSL implementationpublic2016-01-26 08:52
Assigned Toyakobowski 
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0001553: Fails to cope with multiple non-contiguous constant array instantiations
DescriptionFrama-C fails to parse the following legitimate C code:

struct a {
    int b;
struct a *d[] = {&(struct a){1}};
int wibble(void)
{ return 1; }
struct a *e[] = {&(struct a){1}};

The error message returned is:
[kernel] preprocessing with "gcc -C -E -I. test.c"
test.c:12:[kernel] user error: Global __constr_expr_0 was already defined at test.c:5
[kernel] user error: skipping file "test.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
TagsNo tags attached.
Attached Files




gergo (reporter)

I stumbled across the same problem in Sodium-20150201, where it is still present. The apparent fix is trivial:

--- ../frama-c-Sodium-20150201/cil/src/frontc/cabs2cil.ml 2015-03-06 16:28:27.000000000 +0100
+++ cil/src/frontc/cabs2cil.ml 2015-06-23 20:54:47.133240542 +0200
@@ -7819,7 +7819,6 @@
       !currentFunctionFDEC.svar.vdecl <- idloc;
- constrExprId := 0;
           (* Setup the environment. Add the formals to the locals. Maybe
            * they need alpha-conv *)
           enterScope (); (* Start the scope *)

This code used to reset that counter every time a function definition was entered; removing that reset changes nothing except that it ensures that the generated __constr_expr_ variables have globally unique names (even across files). The counter is not used for anything else but for making these variable names unique. Possibly it should be reset when previously read source files are re-parsed, I don't know.


yakobowski (manager)

Your patch is correct. We arrived at the same fix a few years back, but forgot to commit it. Apologies for this... The fix will be in the next version of Frama-C.

(Resetting the counter at the beginning of a file is slightly better, because the generated numbers will be more predictable.)


yakobowski (manager)

Fix committed to master branch.

-Issue History
Date Modified Username Field Change
2013-11-08 03:52 BluewaterSys New Issue
2013-11-08 03:52 BluewaterSys Status new => assigned
2013-11-08 03:52 BluewaterSys Assigned To => virgile
2013-11-08 08:42 virgile Status assigned => confirmed
2015-06-23 21:02 gergo Note Added: 0005942
2015-08-03 19:42 yakobowski Note Added: 0005990
2015-08-03 19:42 yakobowski Source_changeset_attached => framac master 594b4825
2015-08-03 19:42 yakobowski Note Added: 0005991
2015-08-03 19:42 yakobowski Assigned To virgile => yakobowski
2015-08-03 19:42 yakobowski Status confirmed => resolved
2015-08-03 19:42 yakobowski Resolution open => fixed
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed
+Issue History