pretty-printed program rejected by GCC. Affects -print, slicing, scf (csmith)
ID0000810: This issue was created automatically from Mantis Issue 810. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000810 | Frama-C | Kernel | public | 2011-05-02 | 2014-02-12 |
| Reporter | pascal | Assigned To | monate | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20110201 | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
$ cat const_field_return_struct.c struct S { const int f0; int f1; } T, U;
struct S f(int c) { if (c) return T; return U; } $ frama-c -quiet -print const_field_return_struct.c > t.c $ cat t.c /* Generated by Frama-C / struct S { int const f0 ; int f1 ; }; struct S T ; struct S U ; struct S f(int c ) { struct S __retres ; if (c) { __retres = T; goto return_label; } __retres = U; return_label: / internal */ return (__retres); } $ gcc t.ct.c: In function 'f': t.c:11: error: assignment of read-only variable '__retres' t.c:12: error: assignment of read-only variable '__retres'