--- layout: fc_discuss_archives title: Message 94 from Frama-C-discuss on March 2009 ---
Hellom On Thu, Mar 26, 2009 at 16:59, PAREAUD, Thomas <Thomas.PAREAUD at astrium.eads.net> wrote: > Is the 3) point is equivalent to add the predicate below in the loop invariant declaration? > > loop invariant > ? ? ?[...] > ? && \forall integer k ; 0 <= k < (\at(nbBytes, Pre) - nbBytes) ==> (*(\at(pString1, Pre)+k) == *(\at(pString2, Pre)+k)); > > This line is equivalent to the following one: > > \forall integer k ; 0 <= k < (\at(nbBytes, Pre) - nbBytes) ==> (*(pString1-k) == *(pString2-k)); Are you able to prove the preservation part of these two loop invariants? It fails with Alt-Ergo. Yours, d.