# 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

*Subject*: [Frama-c-discuss] RE : Behaviour allowing to prove 1==2*From*: dmentre at linux-france.org (David MENTRE)*Date*: Mon, 16 Dec 2013 11:56:22 +0100*In-reply-to*: <9714BB54B80D7946B2C6265DCB0AE1491A6AF144@EXDAG0-B0.intra.cea.fr>*References*: <52AB23FE.7030701@linux-france.org> <9714BB54B80D7946B2C6265DCB0AE1491A6AF144@EXDAG0-B0.intra.cea.fr>

Hello Lo?c, Le 16/12/2013 11:11, CORRENSON Loic 218851 a ?crit : > 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. Yes. We are going to simplify those annotations following you remarks. > 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. Well, we don't think the generated PO are correct, for at least some of them. If you look at the attached file, we are able to prove x > 0 and x < 0 in a row within the switch case. In fact, both VC have "Have: false" in hypothesis. This is how we discovered the issue, in our real code we have more complex code in the switch cases and they were proved a bit too easily. :-) > I suspect the bug to come from late simplification stage of WP. > Using -wp-no-let turns off the bug. Thanks, that gives us a workaround. > I opened an issue in the BTS :http://bts.frama-c.com/view.php?id=1586 Thanks, I have added this example. Best regards, david -------------- next part -------------- typedef enum {N, A, B} trans_t; /*@ behavior more_than_five: assumes x > 5; ensures x > 5 <==> \result == A; behavior less_than_five: assumes x >= 0 && x <= 5; ensures (x >= 0 && x <= 5) <==> \result == B; behavior none: assumes x < 0; ensures x < 0 <==> \result == N; complete behaviors; disjoint behaviors; */ trans_t compute_trans(int x) { if (x > 5) return A; else if (x >= 0) return B; else return N; } /*@ behavior more_than_five: assumes x > 5; ensures x > 5 ==> \result == A; behavior less_than_five: assumes x >= 0 && x <= 5; ensures (x >= 0 && x <= 5) ==> \result == B; behavior none: assumes x < 0; ensures x < 0 ==> \result == N; complete behaviors; disjoint behaviors; */ trans_t compute_trans2(int x) { if (x > 5) return A; else if (x >= 0) return B; else return N; } /*@ ensures \result == -1 || \result == 1 || \result == 2; */ int main(int x) { trans_t trans = N; trans = compute_trans(x); switch(trans) { case N: //@ assert x < 0; //@ assert x > 0; return -1; break; case A: return 1; break; case B: return 2; break; default: return -1; break; } }

**References**:**[Frama-c-discuss] Behaviour allowing to prove 1==2***From:*dmentre at linux-france.org (David MENTRE)

**[Frama-c-discuss] RE : Behaviour allowing to prove 1==2***From:*loic.correnson at cea.fr (CORRENSON Loic 218851)

- Prev by Date:
**[Frama-c-discuss] RE : Behaviour allowing to prove 1==2** - Next by Date:
**[Frama-c-discuss] New Version of "ACSL by Example" for Frama-C Fluorine** - Previous by thread:
**[Frama-c-discuss] RE : Behaviour allowing to prove 1==2** - Next by thread:
**[Frama-c-discuss] New Version of "ACSL by Example" for Frama-C Fluorine** - Index(es):