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

[Frama-c-discuss] Predicates with bitwise operators?



Hi,

I wrote the following

  //@ predicate is_power_2(integer x) = x >= 0 && ((x & (x-1)) == 0);

and I'm trying to test it (Typed+cint) with

  //@ assert is_power_2(2);
  //@ assert is_power_2(8);
  //@ assert is_power_2(4);
  //@ assert is_power_2(64);
  //@ assert !is_power_2(66);

Unfortunately, WP does not seem to find a proof for any of them. Any ideas?