| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001553 | Frama-C | Kernel > ACSL implementation | public | 2013-11-08 03:52 | 2016-01-26 08:52 | ||||
| Reporter | BluewaterSys | ||||||||
| Assigned To | yakobowski | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Fluorine-20130601 | ||||||||
| Target Version | Fixed in Version | Frama-C Magnesium | |||||||
| Summary | 0001553: Fails to cope with multiple non-contiguous constant array instantiations | ||||||||
| Description | 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. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
gergo (reporter) 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/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) 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.) |
|
yakobowski (manager) 2015-08-03 19:42 |
Fix committed to master branch. |
| Notes |
| 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 |