--- layout: fc_discuss_archives title: Message 13 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?



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