Slicing leaves unreachable code
ID0000194:
**This issue was created automatically from Mantis Issue 194. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000194 | Frama-C | Plug-in > slicing | public | 2009-07-15 | 2009-08-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | Anne | **Resolution** | no change required |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
/*@ requires
@ (((v1 && !(v2 && v3) && v4);
@*/
extern void fun(void)
{
if (v1) {
if (v4) {
if (v2) {
if(v3) {goto return_label;}
}
}
}
}
### Additional Information :
It would be nice if slicing could remove such code.
issue