--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on August 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Proving properties with land?



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