# 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] Behaviour allowing to prove 1==2

*Subject*: [Frama-c-discuss] Behaviour allowing to prove 1==2*From*: dmentre at linux-france.org (David MENTRE)*Date*: Fri, 13 Dec 2013 16:13:02 +0100

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 -------------- 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 1==2; return -1; break; case A: return 1; break; case B: return 2; break; default: return -1; break; } }

**Follow-Ups**:**[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] ACSL annotation for making function calls** - Next by Date:
**[Frama-c-discuss] New Version of "ACSL by Example" for Frama-C Fluorine** - Previous by thread:
**[Frama-c-discuss] ACSL annotation for making function calls** - Next by thread:
**[Frama-c-discuss] RE : Behaviour allowing to prove 1==2** - Index(es):