--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on December 2011 ---
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>