--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on September 2017 ---
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