--- layout: fc_discuss_archives title: Message 94 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Named behavior, proof obligations and ACSL annotations: the string comparison example



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.