--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on December 2013 ---
Hi, Thanks for the report. It seems to be bug, but I should investigate more the situation. Few remarks, however: Due to WP simplifications, (assert 1==2) is always translated locally in (assert \false). In the behaviors, repeating the assumes clause in the requires, be it with (==>) or (<==>) is useless. In the generated proof obligations, removing the (assert \false) clause, you can see that all then generated proof obligations are correct, using the two variants (with ==> or with <==>). Moreover, you can notice that in the (==>) case, the assumes clause is not repeated. I suspect the bug to come from late simplification stage of WP. Using -wp-no-let turns off the bug. I opened an issue in the BTS : http://bts.frama-c.com/view.php?id=1586 Regards, L. ________________________________________ De : frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] de la part de David MENTRE [dmentre at linux-france.org] Date d'envoi : vendredi 13 d?cembre 2013 16:13 ? : Frama-C public discussion Objet : [Frama-c-discuss] Behaviour allowing to prove 1==2 Hello, 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. When 1==2 is proved, it appears that we have "Have: false" in corresponding VC, as if all the cases in the switch were considered not taken. We have two questions: 1. Could somebody explain us what is really occurring in this case? We do not understand from where the contradiction is coming from. 2. Is there a methodology to avoid this situation? I though than when everything is green without any assumption, then we are sure that everything is correct. Best regards, david