Switch statements seem to be unsound
ID0002246: This issue was created automatically from Mantis Issue 2246. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002246 | Frama-C | Plug-in > wp | public | 2016-08-19 | 2016-12-05 |
| Reporter | ghulette | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | Linux | OS Version | Ubuntu 16.04 |
| Product Version | Frama-C Aluminium | Target Version | - | Fixed in Version | - |
Description :
// Run the following to see the problem: // $ frama-c -wp -wp-rte bad.c // // Frama-C does not detect the error in the ensures condition. You // can cause WP to report the error by commenting out the case 0 line, // or by passing the -simplify-cfg option. Maybe a problem with // switch statements?
int x;
/*@ requires x != 1; assigns x; ensures x != 1; */ void bad (int e) { switch (e) { case 0: break; case 1: x = 1; break; } }
Additional Information :
$ frama-c --version Aluminium-20160501
Steps To Reproduce :
See comments in description.