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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information