--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on December 2013 ---
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; } }