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

Previous Next

Full log

View this message in rfc822 format

From: DAVID MONNIAUX <david.monniaux <at> univ-grenoble-alpes.fr>
To: 34220 <at> debbugs.gnu.org
Subject: bug#34220: 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)]

Previous Next

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