Andrew Haley <aph@xxxxxxxxxx> writes: > I've just checked, and the 64-bit glibc version of sincos does indeed > do > > ENTRY (BP_SYM (__sincos)) > ENTER > > movsd %xmm0, -8(%rsp) > fldl -8(%rsp) > fsincos > ... Thank you all very much for clarifying this issue. I am very much surprised that x87 instructions behave differently on AMD and Intel processors but this seems indeed to be the case. I found the following article (especially section 4.1) helpful: D. Monniaux, "The Pitfalls of Verifying Floating-Point Computations", http://dx.doi.org/10.1145/1353445%2E1353446
