bug#34220: failure to building with CompCert, patch proposed

[Paul Eggert]

DAVID MONNIAUX wrote:
> under CompCert, floating-point values are not simplified at compile time (due 
> to concerns that this simplification may differ from the operations on the 
> target platform).

This concern is incorrect for the expression ((int) 1.5 == 1), which must yield 
1 regardless of floating point format or rounding mode on any practical platform 
(indeed, on any platform that conforms to the C standard, as I understand it).

Also, by reporting an error in this context the CompCert compiler violates the C 
standard, which says that ((int) 1.5 == 1) is an integer constant expression and 
so must be accepted in this context. See section 6.6 paragraph 6 of the C11 
standard (which is the same as C99 in this area).

> +#ifdef __COMPCERT__ 
> +#define TYPE_IS_INTEGER(t) 1 
> +#else 
> #define TYPE_IS_INTEGER(t) ((t) 1.5 == 1) 
> +#endif 

I'd rather not do that. This part of the code has been stable for years and 
works correctly on hundreds of practical C compilers, and I worry that we'd need 
to make similar changes elsewhere to work around the CompCert compiler bug. 
Instead, please file a bug report for CompCert so that its maintainers can fix 
the bug in the compiler. Thanks.