GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0001425	Frama-C	Plug-in > Eva	public	2013-05-23	2013-05-23

Reporter	Anne	Assigned To	yakobowski	Resolution	no change required
Priority	normal	Severity	feature	Reproducibility	N/A
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Fluorine-20130401	Target Version	-	Fixed in Version	-

Description :

It might be interesting that the Value analysis emit a message when it detect that the program point after a loop or a call is unreachable.

Just an idea...

Additional Information :

Example: void may_be_infinite (int c) { int x = 0; if (c > 0) { while (1) ; x = 1; // <-- unreachable } } void main (int cond) { int r = 0; if (cond > 0) { may_be_infinite (cond); r = 1; // <-- unreachable } else { may_be_infinite (cond); r = 2; } }