Skip to content

Incorrect handling of nearly-empty switch clauses with -simplify-cfg

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


Id Project Category View Due Date Updated
ID0000720 Frama-C Kernel public 2011-02-13 2014-02-12
Reporter yakobowski Assigned To virgile Resolution fixed
Priority normal Severity crash Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Carbon-20110201 Target Version - Fixed in Version Frama-C Nitrogen-20111001

Description :

Frama-c chokes on the following code with option -simplify-cfg

void main() { switch(0) { case 0: break; } }

This can be seen either by starting the value analysis, or with -check.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information