Bug in let-elimination (due to <==> and assert false).
ID0001586: This issue was created automatically from Mantis Issue 1586. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001586 | Frama-C | Plug-in > wp | public | 2013-12-16 | 2014-03-13 |
| Reporter | correnson | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C Neon-20140301 |
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.