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;
}

main(){
  int An, Bn, in, jn;
  float A, B, i, j;
  for (An=-26; An<26; An++)
    {
      A = Frama_C_float_interval(An / 8., (An + 1) / 8.);
      for (Bn=-26; Bn<26; Bn++)
	{
	  B = Frama_C_float_interval(Bn / 8., (Bn + 1) / 8.);
	  for (in=-26; in<26; in++)
	    {
	      i = Frama_C_float_interval(in / 8., (in + 1) / 8.);
	      for (jn=-26; jn<26; jn++)
		{
		  j = Frama_C_float_interval(jn / 8., (jn + 1) / 8.);
		  compute(A, B, i, j);
		}
	    }
	}
    }
}