--- layout: fc_discuss_archives title: Message 69 from Frama-C-discuss on August 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Proving a simple property on bitshift with WP



Hello David,

2013/8/29 David MENTRE <dmentre at linux-france.org>:

>
> I have tried to use a more detailed memory model with "-wp-model
> "Typed,int" " without success.
>
> I am using Frama-C Fluorine 20130501, Why3 0.81 and Alt-Ergo 0.95.1.
>
> ===
> static unsigned char m[] = {
>   (1 << 7),
>   (1 << 6),
>   (1 << 5),
>   (1 << 4),
>   (1 << 3),
>   (1 << 2),
>   (1 << 1),
>   (1 << 0)
> };
>
> /*@ requires n >= 0;
>  */
> int main(int n)
> {
>   int size, bit;
>
>   size = 8;
>   bit = n%size;
>   //@ assert 0 <= bit <= 7;
>
>   //@ assert m[0] == ((unsigned char)(1 << 7));
>   //@ assert m[bit] == ((unsigned char)1 << (7-(n%8)));
>
>   return 0;
> }

I'm afraid that WP tries to play it a bit too smart here: if you look
at the generated goal, you'll see that the values of the m[i] have
been const-folded, so that you have m[0] == 128, m[1] == 64, etc. It
makes the assert on m[0] trivial, but
the assert on m[bit] much more complicated, as the prover somehow has
to revert back the transformation. Since we're dealing with a bitwise
rather than an arithmetic operation, I'm not sure that there's an easy
way to have alt-ergo prove that. Options -wp-no-simpl and -wp-nolet do
not seem to have an impact on the transformations made by WP.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile