float64_t __float64_add(float64_t augend, float64_t addend);
__float64_add adds addend to augend and returns the sum as the result.