fptrunc and undefined results


The LangRef says this about fptrunc:

“The ‘fptrunc‘ instruction truncates a value from a larger floating point type to a smaller floating point type. If the value cannot fit within the destination type, ty2, then the results are undefined.”

What does it mean for the value to “fit within the destination type”? For instance, is the value of

%Inf = fptrunc double 0x7FF0000000000000 to float

defined? This happens to be folded to a float infinity right now.

The LangRef gives this as an example:

%Y = fptrunc double 1.0E+300 to float ; yields undefined

but this is incompatible with C11 Annex F (IEC 60559 floating-point arithmetic), which says:

“Since negative and positive infinity are representable in IEC 60559 formats, all real numbers lie within the range of representable values.”

This implicitly makes all float-to-float conversions have defined behavior in a C11 implementation which follows Annex F, since the value is always within the range of representable values of the destination type.

So… is the result of fptrunc in this situation really undefined, and should it be? How should it behave on Infs and NaNs?