Thank you! Marcelo.
I've got it: in c doubles are passed to a function by pushing its two
dword parts: first the high and then the low part, and when it's the
result of a double type function is returned in the ST0 of the FPU.
