Skip to content

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