--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on August 2017 ---
I have the following simple function int test(unsigned char x) { int y; y = (int)x & 0x5; //@ assert 0 <= (x & 0x1); //@ assert 0 <= (x & 0x4); return y; } The first assertion goes through but the second one cannot be proved. My options: -wp -wp-rte -wp-init-const -wp-model ref -wp-split Eventually, I want to prove something more complicated such as /*@ lemma alignment: \forall integer x, y; x <= y && y % 4 == 0 ==> ((x + 3) & 4) <= y; @*/ But I can't even get a simple toy property proven. Thanks, Yifan