// De Claude Marché et JC Filliâtre (https://toccata.gitlabpages.inria.fr/toccata/gallery/BinarySearchACSL.fr.html)
// inspiré d'un vrai bug chez Google (https://research.google/blog/extra-extra-read-all-about-it-nearly-all-binary-searches-and-mergesorts-are-broken/)

// Version avec post-condition complète!
// à tester avec frama-c -wp -wp-rte -wp-split signed_binary_search_full.c

/*@ requires 0 <= n && \valid_read(t+(0..n-1))
  @   && \forall int i,j; 0 <= i <= j < n ==> t[i] <= t[j];
  @ assigns \nothing;
  @ ensures (0 <= \result < n && t[\result] == v) ||
  @  (\result == -1 &&
  @     \forall int 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;
    @ loop invariant \forall int k; 0 <= k < n && t[k] == v ==> l <= k <= u;
    @ loop assigns l, u; */
  while (l <= u ) {
    int m = l + (u - l) / 2;
    if (t[m] < v) l = m + 1;
    else if (t[m] > v) u = m - 1;
    else return m;
  }
  return -1;
}