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/