Loop variant which does not always decrease passed the verification

ID0000533: This issue was created automatically from Mantis Issue 533. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000533	Frama-C	Plug-in > jessie	public	2010-07-08	2010-09-29

Reporter	logan	Assigned To	cmarche	Resolution	no change required
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Boron-20100401	Target Version	-	Fixed in Version	-

Description :

I have written an implementation of Binary Search and tried to verify it with Frama-C Jessie plug-in. My code passed the verification process but in some cases the loop won't stop. (These cases can be checked by both gcc and hand-calculation.)

There's the loop and its variant: (reference the attachment for the complete source code)

/*@ loop invariant \valid_range(array, left, right);
    loop invariant left <= right;
    loop invariant diff == right - left;
    loop invariant \forall integer i; 0 <= i <= left ==> array[i] != key ;
    loop invariant \forall integer i; right <= i < n ==> array[i] != key ;
    loop variant diff; // NOTICE HERE
*/
while (diff > 0) { // FIXME: This line is INCORRECT actually.
                   // Change to while (diff > 1) for correct version.

    unsigned int mid = left + (right - left) / 2;

    // FIXME: Since (right - left) / 2 will be rounded-off,
    // it is possible that the value of left and right will
    // NEVER be updated.

    if (array[mid] == key) { return mid; }
    else if (array[mid] < key) { left = mid; }
    else { right = mid; }

    diff = right - left;
}

---

REPRODUCE PROCEDURE:

1. Download bisearch.c
2. Start Frama-C/Jessie with: $ frama-c -jessie bisearch.c
3. Click on "Alt-Ergo 0.91"
4. All proof obligations are GREEN.

EXPECTED RESULT:

The proof obligations for "Function bsearch Safety > variant decreases" should result in either FALSE or Time Limit Exceed.

GOT RESULT:

Alt-Ergo 0.91 returns TRUE for such proof obligations.

Additional Information :

I am using the precompiled Frama-C executables from Debian/sid (i386) repository.

VERSION: Frama-C: Boron-20100401 (deb-version: 20100401+boron+dfsg-3) Why: 2.26 (deb-version: 2.26+dfsg-1+b1) Alt-Ergo: 0.91 (deb-version: 0.91-2)

Attachments

• bisearch.c