0000059: code normalisation issue when return variable is named __retres

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000059

Frama-C

Kernel

public

2009-04-23 18:37

2014-02-12 16:56

Reporter

ddelmas

Assigned To

monate

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Lithium-20081201

Target Version

Fixed in Version

Frama-C Beryllium-20090601-beta1

Summary

0000059: 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.

Tags

No 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