--- layout: fc_discuss_archives title: Message 33 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,

I think I discovered a bug:
Following function:

/*@
 requires 0 < length;
*/
int loopinvariant(int length)
{
// loop 1: proof of false specification 
 int i = 0;
 /*@
     loop invariant 0 <= i < length;
 */
 while(++i != length)
 {}
 
// loop 2: proof failed for intended specification 
 i = 0;
 /*@
     loop invariant 0 <= i <= length;
 */
 while(++i != length)
 {}
 
// loop 3: proof of rewritten loop 2
 i = 0;
 i++;
 /*@
     loop invariant 0 <= i <= length;
 */
 while(i != length)
 {
 i++;
 }
 return 0;
}

As you can see from my comments, I expect loop 2 to be correct.

It is courious, that  a weaker loop invariant fails.

But loop 1 is falsly specifyed but proven never the less.

I think this is of interest and please tell me if I misinterpreted something

Cheers

Christoph
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090122/97a0c9c3/attachment.htm