View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001586 | Frama-C | Plug-in > wp | public | 2013-12-16 11:10 | 2014-03-13 15:57 | ||||
Reporter | correnson | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | major | Reproducibility | have not tried | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | |||||||||
Target Version | Fixed in Version | Frama-C Neon-20140301 | |||||||
Summary | 0001586: Bug in let-elimination (due to <==> and assert false). | ||||||||
Description | Bug in let-elimination (due to <==> and assert false). Using -wp-no-let makes the assert false not-proved as expected. | ||||||||
Additional Information | In the attached program, we have no assumption and everything is proved with WP (Frama-C Fluorine June), including the assert 1==2 in case N! frama-c-gui -pp-annot -wp -wp-rte q19_switch_fun_call.c It appears that the issue is coming from the equivalences used in the behaviours of compute_trans(). If we replace "<==>" by "==>", then the 1==2 assert is not proved (substitute call to compute_trans() by compute_trans2() in main()). In both cases (compute_trans() and compute_trans2()), the contract is always proved. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
dmentre (reporter) 2013-12-16 11:46 |
Another example added. VC for "assert x > 0;" has False in hypothesis. |
correnson (manager) 2014-02-05 16:29 |
Fix committed to master branch. |
correnson (manager) 2014-02-12 16:57 |
Fix committed to stable/neon branch. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2013-12-16 11:10 | correnson | New Issue | |
2013-12-16 11:10 | correnson | Status | new => assigned |
2013-12-16 11:10 | correnson | Assigned To | => correnson |
2013-12-16 11:10 | correnson | File Added: q19_switch_fun_call.c | |
2013-12-16 11:45 | dmentre | File Added: q20_switch_fun_call.c | |
2013-12-16 11:46 | dmentre | Note Added: 0004377 | |
2014-02-05 16:29 | correnson | Source_changeset_attached | => framac master 65bc56b6 |
2014-02-05 16:29 | correnson | Note Added: 0004505 | |
2014-02-05 16:29 | correnson | Status | assigned => resolved |
2014-02-05 16:29 | correnson | Resolution | open => fixed |
2014-02-12 16:53 | correnson | Source_changeset_attached | => framac stable/neon 65bc56b6 |
2014-02-12 16:57 | correnson | Note Added: 0004533 | |
2014-03-13 15:56 | signoles | Fixed in Version | => Frama-C Neon-20140301 |
2014-03-13 15:57 | signoles | Status | resolved => closed |