test_a_float128_z_floatx80
test_a_float128_z_floatx80( floatx80 ( float128 ), floatx80 ( float128 ) );
test_a_float128_z_floatx80(