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.
