Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000059Frama-CKernelpublic2009-04-23 18:372014-02-12 16:56
Reporterddelmas 
Assigned Tomonate 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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

-  Notes
There are no notes attached to this issue.

- 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 Checkin
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker