Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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