Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] how to abstract the loop invariants of C

Hello, again.

2011/12/28 ?? <luoting8609 at 163.com>

> But I don't  know the strategically placed annotation. Would you please
> give me more information about this? Where is " .../tests/float/round10d.i
> " ?
>

It is just a test file in the source distribution. However, please
disregard this advice.
In your source code, if you wished to remove the loops and save yourself
the writing of loop invariants, it would be simpler to define FULL_UNROLL.

Take the example of the piece of code line 699 and onwards.

/*@ ghost u32 E = s0;*/
...
/*@ loop invariant (0<=r<=Nr/2) &&
   ( t0 == (Te0[(E >> 24)]  ^ ...
*/
    for (;;) {
        t0 =
            Te0[(s0 >> 24)       ] ^
            Te1[(s1 >> 16) & 0xff] ^
            Te2[(s2 >>  8) & 0xff] ^
            Te3[(s3      ) & 0xff] ^
            rk[4];
 ...

        s0 =
            Te0[(t0 >> 24)       ] ^
            Te1[(t1 >> 16) & 0xff] ^
            Te2[(t2 >>  8) & 0xff] ^
            Te3[(t3      ) & 0xff] ^
            rk[0];
...
}

This won't work. You gave E the value of s0 before the loop, and you have
written an invariant where, in the property that had a chance to hold, you
substituted "s0" with "E". And the loop modifies s0.
Anyway, you don't want to capture everything the loop does in the
invariant. It does not simplify (or Rijndael would be a very bad cipher
indeed). If you only want to verify the safety of the program, you don't
need to capture precisely how the input buffer is processed. Your invariant
only needs to contain the information necessary to see that the memory
accesses are safe.

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111228/8ab70f25/attachment.htm>