--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on January 2009 ---
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