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 |
|
![]() |
||||||
|
![]() |
|
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 |
![]() |
|||
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 |