May C evaluate with multiple floating-point formats?

Question

C 2011 [N1570] 5.2.4.2.2 9 says:

Except for assignment and cast …, the values yielded by operators with floating operands and values subject to the usual arithmetic conversions and of floating constants are evaluated to a format whose range and precision may be greater than required by the type.

Does this mean all floating-point operations in the implementation may be evaluated with one format or each operation may be evaluated with a format with greater range and precision?

The latter would permit A*B == A*B to evaluate as false, if A*B evaluated with extra precision differed from A*B evaluated with nominal precision.

Answer 1

It is worth reading the interpretation of Joseph S. Myers of the relevant parts of the standard in the case of GCC's C compiler, and the definition of FLT_EVAL_METHOD in C11 5.2.4.2.2:9:

The use of evaluation formats is characterized by the implementation-defined value of FLT_EVAL_METHOD:

-1 indeterminable;

0 evaluate all operations and constants just to the range and precision of the type;

1 evaluate operations and constants of type float and double to the range and precision of the double type, evaluate long double operations and constants to the range and precision of the long double type;

2 evaluate all operations and constants to the range and precision of the long double type.

A C compiler that defines FLT_EVAL_METHOD as -1 does not need to do anything specific regarding the precision of floating-point computations, but according to the above, one that defines it to 1 should only evaluate float expressions in double precision, and one that defines it to 2 should only evaluate float and double expressions in long double precision.

The standard does not explicitly allow other precisions, and neither does it explicitly allow rounding to the nominal precision at the compiler's convenience. (GCC was doing the latter before Joseph S. Myers's patch, and clang -mno-sse2 -std=c99 on x86 was doing the same kind of thing the last time I tried it, while at the same time incorrectly defining FLT_EVAL_METHOD to 0).

According to this strict interpretation of the meaning of FLT_EVAL_METHOD, a * b should only have one value, and if this value is not NaN, a * b == a * b should always hold in a C program compiled with a compiler that defined FLT_EVAL_METHOD to 0, 1 or 2.