Logo Hisseo

Checking if x387 unit is in use

The following code satisfies the assertion ifIEEE754 if the compiler and processor respect strictly the IEEE-754 norm which requires that each single operation is rounded to 64bits.

Otherwise, say when using the x387 unit which computes auxiliary expressions in 80bits registers, the value of variable res is 0x1p52 instead of 0.0

#pragma JessieFloatModel(strict)

/* to enforce 387 instructions, use :

 gcc -mfpmath=387 fp-test2.c && ./a.out


int main() {
  double tmp1= 0x1p53;
  double tmp2= 0x1p52;
  double a = tmp1 - 1.0;
  double b = tmp2 + 1.0;
  double c = tmp1 * tmp2;
  double res = a*b - c;
  //@ assert ifIEEE754: res == 0.0; // in IEEE 754 mode
  // @ assert ifIntel387: res == 0x1p52; // indeed tmp2, in intel 80 bits mode
  printf("a=%a b=%a c=%a res=%a\n",a,b,c,res);
  return 0;

This is proved entirely by Gappa