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 - 2019 MantisBT Team
Powered by Mantis Bugtracker