--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on August 2018 ---
Hi, I'm a grad student of computer science currently playing around with frama-c in their spare time and I've struck one case where I don't understand the behavior of frama-c/wp. Given the following program frama-c/wp cannot prove the assert c_gt_0. Everything else is proven successfully. Intuitively it seems to me that from x >= 0 and x != 0 follows x > 0, and indeed for d that is the case, but not for c. I would like to understand why that is so. $ cat narf.c #include <unistd.h> /*@ @ requires 0 <= d < 256; @*/ size_t test(char foo, unsigned int d) { unsigned int c = (unsigned char)foo; if (c != 0) { //@ assert c_lt_256: c < 256; //@ assert c_ge_0: c >= 0; //@ assert c_ne_0: c != 0; //@ assert _0_le_c: 0 <= c; //@ assert c_gt_0: c > 0; return c + d; } if (d != 0) { //@ assert d_lt_256: d < 256; //@ assert d_ge_0: d >= 0; //@ assert d_ne_0: d != 0; //@ assert d_gt_0: d > 0; return c + d; } return 23; } void main(void) { test(23, 42); } $ frama-c -wp -wp-rte narf.c > [kernel] Parsing narf.c (with preprocessing) > [rte] annotating function main > [rte] annotating function test > [wp] 10 goals scheduled > [wp] [Alt-Ergo] Goal typed_test_assert_c_gt_0 : Unknown (Qed:7ms) (56ms) > [wp] Proved goals: 9 / 10 > Qed: 8 (0.48ms-2ms-12ms) > Alt-Ergo: 1 (9ms) (14) (unknown: 1) $ frama-c --version > Chlorine-20180502 Thank you for any input, Sebastian