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