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