Frama-C Bug Tracking System - Frama-C
View Issue Details
0001553Frama-CKernel > ACSL implementationpublic2013-11-08 03:522016-01-26 08:52
Frama-C Fluorine-20130601 
Frama-C Magnesium 
0001553: Fails to cope with multiple non-contiguous constant array instantiations
Frama-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.
No tags attached.
Issue History
2013-11-08 03:52BluewaterSysNew Issue
2013-11-08 03:52BluewaterSysStatusnew => assigned
2013-11-08 03:52BluewaterSysAssigned To => virgile
2013-11-08 08:42virgileStatusassigned => confirmed
2015-06-23 21:02gergoNote Added: 0005942
2015-08-03 19:42yakobowskiNote Added: 0005990
2015-08-03 19:42yakobowskiNote Added: 0005991
2015-08-03 19:42yakobowskiAssigned Tovirgile => yakobowski
2015-08-03 19:42yakobowskiStatusconfirmed => resolved
2015-08-03 19:42yakobowskiResolutionopen => fixed
2016-01-26 08:51signolesFixed in Version => Frama-C Magnesium
2016-01-26 08:52signolesStatusresolved => closed

2015-06-23 21:02   
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/ 2015-03-06 16:28:27.000000000 +0100 +++ cil/src/frontc/ 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.
2015-08-03 19:42   
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.)
2015-08-03 19:42   
Fix committed to master branch.