2021-01-27 12:34 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000059Frama-CKernelpublic2009-04-23 18:372014-02-12 16:56
Reporterddelmas 
Assigned Tomonate 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in VersionFrama-C Beryllium-20090601-beta1 
Summary0000059: code normalisation issue when return variable is named __retres
Description"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.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-Issue History
Date Modified Username Field Change
2009-04-23 18:37 ddelmas New Issue
2009-04-24 10:28 virgile Status new => assigned
2009-04-24 10:28 virgile Assigned To => virgile
2009-04-27 16:48 monate Assigned To virgile => monate
2009-04-27 17:17 svn
2009-04-27 17:54 signoles Status assigned => closed
2009-04-27 17:54 signoles Resolution open => fixed
2009-04-27 17:54 signoles Fixed in Version => Frama-C Beryllium
2013-12-19 01:13 svn Source_changeset_attached => framac master 9cdb23fc
2014-02-12 16:56 monate Source_changeset_attached => framac stable/neon 9cdb23fc
+Issue History