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. ## Attachments - [q19_switch_fun_call.c](/uploads/fa377321dbdcb32a2de9f013fc50164f/q19_switch_fun_call.c) - [q20_switch_fun_call.c](/uploads/3a712d89800fa2c38926aac03f141f57/q20_switch_fun_call.c)