float64_t __float64_mul_asgn(float64_t *multiplicand,
float64_t multiplier);
__float64_mul_asgn updates the floating-point value pointed to by multiplicand by multiplying it by multiplier. The stored product is returned as the result.