struct point { double x; double y; };

struct point t[] =
  { 0.,    1.,
    0.125, 1.00782267782571089,
    0.25,  1.03141309987957319,
    0.5,   1.1276259652063807,
    1.,    1.54308063481524371,
    2.,    3.76219569108363139,
    5.,    74.2099485247878476,
    10.,   11013.2329201033244 };

/*@
  requires 0. <= x <= 10. ;
  assigns \nothing ;
  ensures 0 <= \result <= 6 ; */
int choose_segment(double x);

/*@ requires 0. <= x <= 10. ; */
double interp(double x)
{
  double x0, x1, y0, y1;
  int i;
  i = choose_segment(x);
  x0 = t[i].x;
  y0 = t[i].y;
  x1 = t[i+1].x;
  y1 = t[i+1].y;
  return (y1 * (x - x0) + y0 * (x1 - x)) / (x1 - x0);
}