GNU bug report logs - #34220
failure to building with CompCert, patch proposed

Previous Next

Full log

Message #8 received at 34220 <at> debbugs.gnu.org (full text, mbox):

From: Paul Eggert <eggert <at> cs.ucla.edu>
To: DAVID MONNIAUX <david.monniaux <at> univ-grenoble-alpes.fr>
Cc: 34220 <at> debbugs.gnu.org, Pádraig Brady <P <at> draigBrady.com>
Subject: Re: bug#34220: failure to building with CompCert, patch proposed
Date: Sun, 27 Jan 2019 20:03:56 -0800

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.

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.