slicing produces uncompilable program when formal used as a local variable

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

---

Id	Project	Category	View	Due Date	Updated
ID0000529	Frama-C	Plug-in > sparecode	public	2010-07-06	2010-12-17

Reporter	pascal	Assigned To	Anne	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Boron-20100401	Target Version	-	Fixed in Version	Frama-C Carbon-20101201-beta1

Description :

Alu:day_2 pascal$ cat s.c main(int x, int y, int z){ int A, B; A = x; y = A; B = y; return B; }

Alu:day_2 pascal$ frama-c -sparecode-analysis s.c ... /* Generated by Frama-C */ int main(int x ) { int A ; int B ; A = x; y = A; B = y; return (B); }

The generated program misses a declaration for y.