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

[Frama-c-discuss] bug with loop invariant, wrong loop invariant gets proven



Hello again,

I would like to clarify something:

Given, that
while(++i != length)
 {}

is equivalent to the following:

and the loop invariant requires that i < length,
 /*@
     loop invariant 0 <= i < length;
 */
while(true) {
    i++;
    if (i == length) break;
}

Why is i allowed to become equal to length?

I remember the ACSL document state, that abnormal termination with a "break" 
it is not required that the loop invariant
holds.

That leaves only one question, are both loops truly equivalent.

Again, Thank you for your help.

Cheers

Christoph