GitLab

ID0000059: This issue was created automatically from Mantis Issue 59. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000059	Frama-C	Kernel	public	2009-04-23	2014-02-12

Reporter	ddelmas	Assigned To	monate	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Lithium-20081201	Target Version	-	Fixed in Version	Frama-C Beryllium-20090601-beta1

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.