Binary search in C annotated in ACSL

This is a C version of Binary Search, annotated in ACSL.

Tools: Frama-C / Jessie

References: The VerifyThis Benchmarks

see also the index (by topic, by tool, by reference, by year)

Here is the annotated source code
```/*@ predicate sorted{L}(long *t, integer a, integer b) =
@    \forall integer i,j; a <= i <= j <= b ==> t[i] <= t[j];
@*/

/*@ requires n >= 0 && \valid_range(t,0,n-1);
@ ensures -1 <= \result < n;
@ behavior success:
@   ensures \result >= 0 ==> t[\result] == v;
@ behavior failure:
@   assumes sorted(t,0,n-1);
@   ensures \result == -1 ==>
@     \forall integer k; 0 <= k < n ==> t[k] != v;
@*/
int binary_search(long t[], int n, long v) {
int l = 0, u = n-1;
/*@ loop invariant
@   0 <= l && u <= n-1;
@ for failure:
@   loop invariant
@   \forall integer k; 0 <= k < n && t[k] == v ==> l <= k <= u;
@ loop variant u-l;
@*/
while (l <= u ) {
int m = (l + u) / 2;
//@ assert l <= m <= u;
if (t[m] < v) l = m + 1;
else if (t[m] > v) u = m - 1;
else return m;
}
return -1;
}
```

The program above is the classical binary search for a given element in an array sorted in increasing order.

This program exposes a long-standing bug, that is the computation of l+u may overflow. When attempting to prove this program with Frama-C/Jessie, the VC corresponding to this overflow cannot be proved.