| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001751 | Frama-C | Plug-in > wp | public | 2014-04-11 22:21 | 2015-03-17 22:18 | ||||
| Reporter | jens | ||||||||
| Assigned To | patrick | ||||||||
| Priority | high | Severity | major | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Neon-20140301 | ||||||||
| Target Version | Fixed in Version | Frama-C Sodium | |||||||
| Summary | 0001751: Frama-C/WP "forgets" a proven assertion | ||||||||
| Description | In the following function void strange_after_shift(unsigned int x) { unsigned int y = x & 1; //@ assert y == 0 || y == 1; //@ assert 0 <= y <= 1; } the first assertion is discharged by Qed but the second assertion (which should also hold) is not discharged with Alt-Ergo. Moreover, when I try to prove it with Coq, then I cannot see any hypothesis that represents the first assertion. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
||||||
|
||||||
 Relationships |
| Notes |
|
|
correnson (manager) 2014-06-02 16:00 |
This is due to an over-confident simplification on bitwise operation, that turns (y == 0 || y == 1) into true, thus making it disappear from the goal / the hypothesis. We have to investigate the issue. As a workaround, simply disable the bitwise simplifications with -wp-no-bits option. |
|
patrick (developer) 2014-06-11 11:29 |
Changes done for 0001750 allows alt-ergo to solve these POs. |
|
patrick (developer) 2014-06-11 11:45 |
The first note given by Loïc is the real explanation of this issue. That should be discussed... |
|
correnson (manager) 2014-09-23 10:17 |
Fixed in related issue |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2014-04-11 22:21 | jens | New Issue | |
| 2014-04-11 22:21 | jens | Status | new => assigned |
| 2014-04-11 22:21 | jens | Assigned To | => correnson |
| 2014-04-11 22:21 | jens | File Added: strange_after_shift.c | |
| 2014-06-02 16:00 | correnson | Note Added: 0005181 | |
| 2014-06-02 16:01 | correnson | Assigned To | correnson => patrick |
| 2014-06-02 16:01 | correnson | Status | assigned => acknowledged |
| 2014-06-02 16:15 | correnson | Relationship added | related to 0001750 |
| 2014-06-11 11:29 | patrick | Note Added: 0005222 | |
| 2014-06-11 11:45 | patrick | Note Added: 0005223 | |
| 2014-09-23 10:17 | correnson | Note Added: 0005482 | |
| 2014-09-23 10:17 | correnson | Status | acknowledged => resolved |
| 2014-09-23 10:17 | correnson | Resolution | open => fixed |
| 2015-03-17 22:17 | signoles | Fixed in Version | => Frama-C Sodium |
| 2015-03-17 22:18 | signoles | Status | resolved => closed |
| Issue History |