double Frama_C_cos_precise(double);
double Frama_C_sin_precise(double);
float Frama_C_float_interval(float, float);

double sin(double x)
{
  return Frama_C_sin_precise(x);
}

double cos(double x)
{
  return Frama_C_cos_precise(x);
}

/*@ ensures 0 <= \result <= 11 ; */
int compute(float A, float B, float i, float j)
{
  float c=sin(i), l=cos(i);
  float d=cos(j), f=sin(j);
  float g=cos(A), e=sin(A);
  float m=cos(B), n=sin(B);

  int N=8*((f*e-c*d*g)*m-c*d*e-f*g-l*d*n);
Frama_C_dump_each();
  return N>0?N:0;
}

int An, Bn, in, jn;

void f(void)
{
  int Ans, Bns, ins, jns;
  float A, B, i, j;
  for (Ans=4*An; Ans<4*(An+1); Ans++)
    {
      A = Frama_C_float_interval(Ans / 32., (Ans + 1) / 32.);
      for (Bns=4*Bn; Bns<4*(Bn+1); Bns++)
	{
	  B = Frama_C_float_interval(Bns / 32., (Bns + 1) / 32.);
	  for (ins=4*in; ins<4*(in+1); ins++)
	    {
	      i = Frama_C_float_interval(ins / 32., (ins + 1) / 32.);
	      for (jns=4*jn; jns<4*(jn+1); jns++)
		{
		  j = Frama_C_float_interval(jns / 32., (jns + 1) / 32.);
		  compute(A, B, i, j);
		}
	    }
	}
    }
}

main(){