Frama-C Bug Tracking System - Frama-C
View Issue Details
0000059Frama-CKernelpublic2009-04-23 18:372014-02-12 16:56
ddelmas 
monate 
normalminoralways
closedfixed 
Frama-C Lithium-20081201 
Frama-C Beryllium-20090601-beta1 
0000059: code normalisation issue when return variable is named __retres
"frama-c file.c -print" outputs non-compilable code for examples such as the following : float g() { double __retres=2; return __retres; } On this example, the output is the following : float g(void) { double __retres ; float __retres ; {__retres = (double )2; __retres = (float )__retres; return (__retres);} } Because of the normalisation scheme, variable __retres is being defined twice, with conflicting types.
No tags attached.
Issue History
2009-04-23 18:37ddelmasNew Issue
2009-04-24 10:28virgileStatusnew => assigned
2009-04-24 10:28virgileAssigned To => virgile
2009-04-27 16:48monateAssigned Tovirgile => monate
2009-04-27 17:17svnCheckin
2009-04-27 17:54signolesStatusassigned => closed
2009-04-27 17:54signolesResolutionopen => fixed
2009-04-27 17:54signolesFixed in Version => Frama-C Beryllium

There are no notes attached to this issue.