--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on July 2017 ---
Hello, The problem is that Qed (the WP simplifier) does not unfold definition on its own, and alt-ergo can not perform bitwise operation. However, in the GUI, you can select your goal and apply the « Definition » tactic which allows Qed to solve the problem. Otherwise, you can turn you predicate into a macro⦠L. > Le 27 juil. 2017 à 19:25, Yifan Lu <me at yifanlu.com> a écrit : > > 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? > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss