--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on April 2009 ---
>> In other words, is this loop invariant correct? > >\at(expr,Pre) always denotes the value of expr in the pre-state of the >function (i.e. when the function is entered). Assuming there's no >overflow or invalid pointer access, the loop invariant is correct. On the subject of the two caveats expressed by Virgile, I would like to add this: 1/ when you subtract two valid pointers with the same base address, the result is never an overflow, so do not worry about that and worry about the validity instead. 2/ Your function presumably has a precondition that looks like "\valid_range(pString, 0, nbBytes)" (perhaps +/-1, I never know). If I was you and if I wasn't able to prove the correctness of my function, one of the things I would try first would be to replicate that precondition inside the invariant: loop invariant i == pString - \at(pString, Pre) && \valid_range(\at(pString, Pre), 0, nbBytes) ; As Virgile explained in another thread, loops are very much treated as opaque blocks by those analyzers that are based on Hoare logic. If you need a property after or even inside the loop, you usually need to put it in the loop invariant, even if it's orthogonal to what the loop does (and it's very easy to forget in this case). Actually it's so annoying that most analyzers try to save you the writing of these parts of the invariant, hence my reserves. It may not be necessary with Jessie. But it doesn't hurt to try. Here's a fun little exercice on the same topic : if you have the property that every cell in an int array t[100] contains 1, what is the invariant for proving that every cell contains 2 after executing the following loop: for (i=0; i<100; i++) t[i]++; Pascal PS: solution in my next post.