Stack overflow when slicing functions invoking themselves circularily

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

---

Id	Project	Category	View	Due Date	Updated
ID0000186	Frama-C	Plug-in > slicing	public	2009-07-14	2014-02-12

Reporter	lukaszc	Assigned To	Anne	Resolution	fixed
Priority	high	Severity	crash	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Beryllium-20090601-beta1	Target Version	Frama-C Boron-20100401	Fixed in Version	Frama-C Boron-20100401

Description :

Stack overflow for the following code:

/@ requires y == 1; @ ensures @ \result == 2y; @/ int x(int y, int z) { //@ assert y == 1; //@ assert y + z == 3; return 2y*z1(); }

int main() { x(1,2); return 0; }

int z1() { return x(2,2); }