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

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 34220 in the body.
You can then email your comments to 34220 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

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

From: DAVID MONNIAUX <david.monniaux <at> univ-grenoble-alpes.fr>
To: bug-coreutils <at> gnu.org
Subject: failure to building with CompCert, patch proposed
Date: Sun, 27 Jan 2019 16:53:27 +0100 (CET)

[Message part 1 (text/plain, inline)]

CompCert (compcert.inria.fr) is a C compiler. 

coreutils test whether some types (e.g. time_t) that it thinks should be integer types (as opposed to floats) using compile-time tricks: 
To test whether T is an integer type, it does (T) 1.5 == 1, and uses the result in the computation of the width of a bitfield, such that if the test is false the width is illegal and produces a compile-time error (this is an old fashioned way of doing a static assert). 

Unfortunately, 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). 
Thus the test always fails. 

Possible fix: 
diff -u -r coreutils-8.30-orig/lib/intprops.h coreutils-8.30/lib/intprops.h 
--- coreutils-8.30-orig/lib/intprops.h 2018-05-14 06:22:34.000000000 +0200 
+++ coreutils-8.30/lib/intprops.h 2019-01-24 14:55:24.567674345 +0100 
@@ -34,7 +34,11 @@ 

/* True if the arithmetic type T is an integer type. bool counts as 
an integer. */ 
+#ifdef __COMPCERT__ 
+#define TYPE_IS_INTEGER(t) 1 
+#else 
#define TYPE_IS_INTEGER(t) ((t) 1.5 == 1) 
+#endif 

/* True if the real type T is signed. */ 
#define TYPE_SIGNED(t) (! ((t) 0 < (t) -1)) 


Directeur de recherche au CNRS, laboratoire VERIMAG, équipe PACSS 
http://www-verimag.imag.fr/~monniaux/ 

[Message part 2 (text/html, inline)]

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.

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

From: Assaf Gordon <assafgordon <at> gmail.com>
To: Paul Eggert <eggert <at> cs.ucla.edu>,
 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: Fri, 8 Feb 2019 14:36:55 -0700

tags 34220 wontfix
close 34220
stop

Hello,

On 2019-01-27 9:03 p.m., Paul Eggert wrote:
> DAVID MONNIAUX wrote:
>> under CompCert, floating-point values are not simplified at compile 
>> time
[...]
> please file a bug report for CompCert so 
> that its maintainers can fix the bug in the compiler.
Given the above, I'm closing this as "won't fix".

Discussion can continue by replying to this thread.

-assaf

Previous Next

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