--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on December 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] RE : Behaviour allowing to prove 1==2



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