Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000810Frama-CKernelpublic2011-05-02 09:472014-02-12 16:59
Reporterpascal 
Assigned Tomonate 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000810: pretty-printed program rejected by GCC. Affects -print, slicing, scf (csmith)
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'
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001837)
pascal (reporter)
2011-05-02 10:45

Interesting remark from Great Leader: ~/ppc $ cat t.c struct S { const int f0; int f1; } T, U; struct S f(int c) { struct S V = { 12, 45 }; return U; } ~/ppc $ bin/toplevel.opt -print t.c [kernel] preprocessing with "gcc -C -E -I. t.c" /* Generated by Frama-C */ struct S { int f0 ; int f1 ; }; struct S T; struct S U; struct S f(int c) { struct S V; V.f0 = 12; V.f1 = 45; return (U); } So the const-removal-when-necessary code is already there, it is enough to make sure the criterion is widened to include the example provided.

- Issue History
Date Modified Username Field Change
2011-05-02 09:47 pascal New Issue
2011-05-02 09:47 pascal Summary pretty-printed program rejected by GCC. Affects -print, slicing, scf => pretty-printed program rejected by GCC. Affects -print, slicing, scf (csmith)
2011-05-02 10:45 pascal Note Added: 0001837
2011-05-02 10:46 pascal Assigned To => monate
2011-05-02 10:46 pascal Status new => assigned
2011-05-02 16:56 svn Checkin
2011-05-02 16:56 svn Status assigned => resolved
2011-05-02 16:56 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2014-02-12 16:59 monate Note Added: 0004797
2014-02-12 16:59 monate Status closed => resolved
2014-03-13 21:58 yakobowski Note Deleted: 0004797


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker