View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002127 | Frama-C | Plug-in > wp | public | 2015-06-04 11:50 | 2016-01-26 08:43 | ||||
Reporter | loic | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | Linux | OS | Ubuntu | OS Version | 12.04.5 LTS | ||||
Product Version | |||||||||
Target Version | Fixed in Version | Frama-C Magnesium | |||||||
Summary | 0002127: Unprovable inequality involving (unsigned) -1 | ||||||||
Description | Nitrogen-20111001 alt-ergo 0.94 The following assertion cannot be proven. void arithmetic_testcase(unsigned i) { /*@ assert i <= (unsigned) -10 ==> i + 9 <= (unsigned) -1; */ } | ||||||||
Steps To Reproduce | frama-c -wp -wp-ret for the code above (also as attachment). | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2015-06-04 11:50 | loic | New Issue | |
2015-06-04 11:50 | loic | Status | new => assigned |
2015-06-04 11:50 | loic | Assigned To | => correnson |
2015-06-04 11:50 | loic | File Added: arithmetic_testcase.c | |
2015-06-29 16:37 | correnson | Note Added: 0005950 | |
2015-06-29 16:38 | correnson | Status | assigned => closed |
2015-06-29 16:38 | correnson | Resolution | open => fixed |
2015-06-29 16:38 | correnson | Fixed in Version | => Frama-C Magnesium |
2015-06-29 16:42 | correnson | Status | closed => resolved |
2016-01-26 08:43 | signoles | Status | resolved => closed |