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 implementation of AES

Hello,

please attach the files as plainly as possible. If your mailer refuses to
let you send .c files under the pretext that it's "executable" and could
carry a virus, please just change the extension.

The header rijndael-alg-fst.h is missing, so I could not try your
annotations.
However, a couple of remarks:


/*@ ghost goto L; */
/*@ ghost L:  */

You are not supposed to use "goto" in a ghost statement. That it is
accepted is a known bug (no need to report it, we know about it).
Especially
here, it does not seem to do anything.

   /*@ loop invariant (0 <= i <=10) &&
    ( rk[4] == ( P ^ (Te4[(S >> 16) & 0xff] & 0xff000000) ^
               (Te4[(S >> 8) & 0xff] & 0x00ff0000) ^
(Te4[(S    ) & 0xff] & 0x0000ff00) ^
(Te4[(S >> 24)     ] & 0x000000ff) ^ T )) &&
     ( rk[5] == (Q ^ rk[4])) &&
     ( rk[6] == (R ^ rk[5])) &&
     ( rk[7] == (S ^ rk[6]));

The above property is not a loop invariant, because rk[7] == (S ^ rk[6]) does
not appear to have any reason to hold before the first iteration, unless I
am missing something. Perhaps you mean i == 0 || ...

You could invent an input vector (any input vector will do) and run a
completely unrolled value analysis. If any pre-condition, post-condition,
assertion or loop invariant is violated, it may be able to tell you about
it, and that may provide a hint.

Bounded loops such as this one may also be unrolled syntactically, which
means that you don't have to provide an invariant for them. Use a
strategically placed annotation:
//@ loop pragma UNROLL 10;

See .../tests/float/round10d.i for an example of use of this annotation.

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