GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0002119	Frama-C	Kernel	public	2015-05-20	2016-01-26

Reporter	hugo.illous	Assigned To	yakobowski	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	-	Target Version	-	Fixed in Version	Frama-C Magnesium

Description :

When a "If" statements contains in its true block the sequence "do {} while (0);", in the CFG, this statement will have only one successor.

Steps To Reproduce :

You can simply try with this C program and compute List.length stmt.succs void f(int n) { if (n == 0) do {} while (0); }