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