Hi nullptr,
printing floating point values via libc under 64 bit Linux is little bit tricky. I've attached for you a simple test program and I hope it'll show you the right direction. The tricky part is to ensure the 16 bit alignment of the stack.
Gerhard