// 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 (presque) uniquement la vérification d'absence de RTE (= UB).
// à tester avec frama-c -wp -wp-rte -wp-split signed_binary_search_rte.c

/*@ requires 0 <= n && \valid_read(t+(0..n-1));
  @ assigns \nothing;
  @ ensures -1 <= \result < n;
  @ ensures \result >= 0 ==> t[\result] == v;*/
int binary_search(long t[], int n, long v) {
  int l = 0, u = n-1 ;
  /*@ loop invariant 0 <= l &&  u < n;
    @ loop assigns l, u; */
  while (l <= u ) {
    int m = (u + l) / 2;
    // FIXME: 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;
}