warning for unreachable program point
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; } }