[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Paul Eggert
Subject: bug#34220: failure to building with CompCert, patch proposed
Date: Sun, 27 Jan 2019 20:03:56 -0800
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.4.0

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.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]