--- layout: fc_discuss_archives title: Message 68 from Frama-C-discuss on January 2014 ---
Hi, Thanks for all responses. I'm not sure why the following code cannot considered invalid; I always get "unknown". Any comments? frama-c -wp -wp-rte non_sense.c -lib-entry int i = 0; /*@ @ behavior BUG: @ assumes i == 5; @ ensures \result == -2; */ int main() { if (0 <= i && i <= 10) { return -1; } if (i == 5) { return -2; } return 0; }