float64_t __float64_mul(float64_t muliplicand, float64_t multiplier);
__float64_mul multiplies multiplicand by multiplier and returns the product as the result.