Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] With Why version 2.23, Jessie binary_search example fails. Why?

  • Subject: [Frama-c-discuss] With Why version 2.23, Jessie binary_search example fails. Why?
  • From: dwheeler at dwheeler.com (David A. Wheeler)
  • Date: Sat, 02 Jan 2010 22:32:02 -0500 (EST)
The Jessie binary_search example works with Why 2.21, but it fails when I try to use Why 2.23.  Is this an error in Why 2.23?  Or, is this an error in the example?  Or, is this a misunderstanding of some kind?

Here are the details:
* I installed Frama-C+Why 2.21; with that, the binary_search example of section 2.1 of the Jessie tutorial worked (http://frama-c.cea.fr/jessie/jessie-tutorial.pdf).  I'm using the "exact" integer model, per the tutorial.  This works well.
* When I downloaded & installed the new Why version 2.23, the same example STOPPED working.  With Why version 2.23, there were 4 more safety VCs named "variant decreases".  Two of the 4 new ones are easily proved by alt-ergo.  But two of the generated VCs try to prove "0<0", which obviously CANNOT be proven.

I installed to the default locations (/usr/local) on a Fedora 12 Linux system, 64-bit x86_64.

Note: This is the *exact* model, so there's no overflow to worry about, and thus the (x+y)/2 should be fine.  In any case, the same problem shows up when I switch this to a bounded integer model and use "m=l + (u-1)/2;".  (The example of section 2.2 has the same problem).

Below is binary_search from section 2.1, which I *believe* is the same as the tutorial example.  (I changed long dashes in the document into "-" since only "-" is accepted).

--- David A. Wheeler

=======================================================

/*@ lemma mean: \forall integer x, y; x <= y ==> x <= (x+y)/2 <= y; */

//@ requires n >= 0 && \valid_range(t,0,n-1);
int binary_search(int* t, int n, int v) {
  int l = 0, u = n-1, p = -1;
  //@ loop invariant 0 <= l && u <= n-1;
  while (l <= u ) {
    int m = (l + u) / 2;
    if (t[m] < v)
      l = m + 1;
    else if (t[m] > v)
      u = m - 1;
    else {
      p = m; break;
    }
  }
  return p;
}