--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on January 2010 ---
[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?



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;
}