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

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



Properties on bitwise operations are difficult to prove by simply using SMT solvers.
However, the Interactive Prover of WP in Frama-C/Gui, might help you. There are several tactics available to transform and/or prove bitwise expressions.
	L.



> Le 15 août 2017 à 23:22, Yifan Lu <me at yifanlu.com> a écrit :
> 
> 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
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss