Convert an integer (r12) to float (f12) in a sane, efficent way?

[jawa]

lets say r12=0000 0006
and i would want to convert it to 0x40c0 0000 (float value of 6)
how would i do that?
i read the Conversion from integer to float in the Working with floats thread, but i didnt get it