From debbugs-submit-bounces@debbugs.gnu.org Sun Jan 27 11:57:51 2019 Received: (at submit) by debbugs.gnu.org; 27 Jan 2019 16:57:51 +0000 Received: from localhost ([127.0.0.1]:47752 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gnnkj-0001OU-Sf for submit@debbugs.gnu.org; Sun, 27 Jan 2019 11:57:51 -0500 Received: from eggs.gnu.org ([209.51.188.92]:50589) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gnmkm-0008GM-0z for submit@debbugs.gnu.org; Sun, 27 Jan 2019 10:53:50 -0500 Received: from lists.gnu.org ([209.51.188.17]:44005) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1gnmkg-0000oh-MZ for submit@debbugs.gnu.org; Sun, 27 Jan 2019 10:53:42 -0500 Received: from eggs.gnu.org ([209.51.188.92]:60788) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gnmkf-0002nn-NS for bug-coreutils@gnu.org; Sun, 27 Jan 2019 10:53:42 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=0.8 required=5.0 tests=BAYES_50,HTML_MESSAGE, RCVD_IN_DNSWL_NONE autolearn=disabled version=3.3.2 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gnmke-0000ne-KZ for bug-coreutils@gnu.org; Sun, 27 Jan 2019 10:53:41 -0500 Received: from zm-mta-out-1.u-ga.fr ([152.77.200.56]:42312) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1gnmkd-0000ii-UY for bug-coreutils@gnu.org; Sun, 27 Jan 2019 10:53:40 -0500 Received: from zm-mta-out.u-ga.fr (zm-mta-out.u-ga.fr [152.77.200.58]) by zm-mta-out-1.u-ga.fr (Postfix) with ESMTP id D250FA02FB for ; Sun, 27 Jan 2019 16:53:27 +0100 (CET) Received: from zm-mbx6.u-ga.fr (zm-mbx6.u-ga.fr [152.77.200.8]) by zm-mta-out.u-ga.fr (Postfix) with ESMTP id CEFB0E009B for ; Sun, 27 Jan 2019 16:53:27 +0100 (CET) Date: Sun, 27 Jan 2019 16:53:27 +0100 (CET) From: DAVID MONNIAUX To: bug-coreutils@gnu.org Message-ID: <623048061.4346963.1548604407813.JavaMail.zimbra@univ-grenoble-alpes.fr> Subject: failure to building with CompCert, patch proposed MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="=_6961fa42-78c0-428e-a35c-96d37a050ce6" X-Originating-IP: [152.77.200.60] X-Mailer: Zimbra 8.7.11_GA_3706 (ZimbraWebClient - FF64 (Linux)/8.7.11_GA_3706) Thread-Index: ztrTDMBXoWSR12Xzz1xzgu87k8faxg== Thread-Topic: failure to building with CompCert, patch proposed X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 152.77.200.56 X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Spam-Score: 0.7 (/) X-Debbugs-Envelope-To: submit X-Mailman-Approved-At: Sun, 27 Jan 2019 11:57:48 -0500 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.3 (/) --=_6961fa42-78c0-428e-a35c-96d37a050ce6 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable CompCert (compcert.inria.fr) is a C compiler.=20 coreutils test whether some types (e.g. time_t) that it thinks should be in= teger types (as opposed to floats) using compile-time tricks:=20 To test whether T is an integer type, it does (T) 1.5 =3D=3D 1, and uses th= e result in the computation of the width of a bitfield, such that if the te= st is false the width is illegal and produces a compile-time error (this is= an old fashioned way of doing a static assert).=20 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).=20 Thus the test always fails.=20 Possible fix:=20 diff -u -r coreutils-8.30-orig/lib/intprops.h coreutils-8.30/lib/intprops.h= =20 --- coreutils-8.30-orig/lib/intprops.h 2018-05-14 06:22:34.000000000 +0200= =20 +++ coreutils-8.30/lib/intprops.h 2019-01-24 14:55:24.567674345 +0100=20 @@ -34,7 +34,11 @@=20 /* True if the arithmetic type T is an integer type. bool counts as=20 an integer. */=20 +#ifdef __COMPCERT__=20 +#define TYPE_IS_INTEGER(t) 1=20 +#else=20 #define TYPE_IS_INTEGER(t) ((t) 1.5 =3D=3D 1)=20 +#endif=20 /* True if the real type T is signed. */=20 #define TYPE_SIGNED(t) (! ((t) 0 < (t) -1))=20 Directeur de recherche au CNRS, laboratoire VERIMAG, =C3=A9quipe PACSS=20 http://www-verimag.imag.fr/~monniaux/=20 --=_6961fa42-78c0-428e-a35c-96d37a050ce6 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
CompCert (compcert.inria.fr) is a C compile= r.

coreutils test whether= some types (e.g. time_t) that it thinks should be integer types (as oppose= d to floats) using compile-time tricks:
To test whether T is = an integer type, it does (T) 1.5 =3D=3D 1, and uses the result in the compu= tation 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 value= s are not simplified at compile time (due to concerns that this simplificat= ion 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
 #def= ine TYPE_IS_INTEGER(t) ((t) 1.5 =3D=3D 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, =C3=A9quipe PACSS
http://www-verimag.imag= .fr/~monniaux/
--=_6961fa42-78c0-428e-a35c-96d37a050ce6-- From debbugs-submit-bounces@debbugs.gnu.org Sun Jan 27 23:04:06 2019 Received: (at 34220) by debbugs.gnu.org; 28 Jan 2019 04:04:06 +0000 Received: from localhost ([127.0.0.1]:48134 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gny9W-0004s6-GN for submit@debbugs.gnu.org; Sun, 27 Jan 2019 23:04:06 -0500 Received: from zimbra.cs.ucla.edu ([131.179.128.68]:49772) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gny9T-0004rb-Sd for 34220@debbugs.gnu.org; Sun, 27 Jan 2019 23:04:05 -0500 Received: from localhost (localhost [127.0.0.1]) by zimbra.cs.ucla.edu (Postfix) with ESMTP id 61FB41611CF; Sun, 27 Jan 2019 20:03:57 -0800 (PST) Received: from zimbra.cs.ucla.edu ([127.0.0.1]) by localhost (zimbra.cs.ucla.edu [127.0.0.1]) (amavisd-new, port 10032) with ESMTP id rCiqYuZPupa6; Sun, 27 Jan 2019 20:03:56 -0800 (PST) Received: from localhost (localhost [127.0.0.1]) by zimbra.cs.ucla.edu (Postfix) with ESMTP id 768C3161215; Sun, 27 Jan 2019 20:03:56 -0800 (PST) X-Virus-Scanned: amavisd-new at zimbra.cs.ucla.edu Received: from zimbra.cs.ucla.edu ([127.0.0.1]) by localhost (zimbra.cs.ucla.edu [127.0.0.1]) (amavisd-new, port 10026) with ESMTP id ffiwtRodjcIN; Sun, 27 Jan 2019 20:03:56 -0800 (PST) Received: from [192.168.1.9] (cpe-23-242-74-103.socal.res.rr.com [23.242.74.103]) by zimbra.cs.ucla.edu (Postfix) with ESMTPSA id 4C713161167; Sun, 27 Jan 2019 20:03:56 -0800 (PST) Subject: Re: bug#34220: failure to building with CompCert, patch proposed To: DAVID MONNIAUX References: <623048061.4346963.1548604407813.JavaMail.zimbra@univ-grenoble-alpes.fr> From: Paul Eggert Organization: UCLA Computer Science Department Message-ID: <41c2e15f-ba21-3307-d9d7-facc3cbe99b5@cs.ucla.edu> 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 MIME-Version: 1.0 In-Reply-To: <623048061.4346963.1548604407813.JavaMail.zimbra@univ-grenoble-alpes.fr> Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: en-US Content-Transfer-Encoding: 7bit X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 34220 Cc: 34220@debbugs.gnu.org, =?UTF-8?Q?P=c3=a1draig_Brady?= X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) 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. From debbugs-submit-bounces@debbugs.gnu.org Fri Feb 08 16:37:08 2019 Received: (at 34220) by debbugs.gnu.org; 8 Feb 2019 21:37:08 +0000 Received: from localhost ([127.0.0.1]:40211 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gsDpc-00078R-KJ for submit@debbugs.gnu.org; Fri, 08 Feb 2019 16:37:08 -0500 Received: from mail-pl1-f182.google.com ([209.85.214.182]:44350) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gsDpY-00077o-GQ; Fri, 08 Feb 2019 16:37:05 -0500 Received: by mail-pl1-f182.google.com with SMTP id p4so2282008plq.11; Fri, 08 Feb 2019 13:37:04 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:cc:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:content-transfer-encoding; bh=RTa6LzR7yxsEYxaWCFwuj3D76Cj2BL9uoiJQj/q480g=; b=hciVrzxABTW8y7f1BhhLjMVs3cGQSUvk7DPK1roFUWNfTIgmOMKoLBMBUbhIpDjL5h YYfwlO3GlcqdEoSj3bgj4brA/hgRfDHAF+acRGkBDR57KokiaP9wJ1pe+fSKegp67fU7 a+oZQorV1OcNUc+ugKFjyM9VG//Ma7bXg8eVnlGaWZIZFcGzDtnDp1Y4JWtDt7MIFMI2 ek4apqeXRbpDtAz3+Er+gjGEYa4VaLxfotjuVV3+V8MVPit1WDdTIwWwgO9DQ/b2DNyx YAfk0ZB+nSOCVQnnL07scbnEQVnfdHieFOD08ZrhA6fPfnR+7hR2BY0cPBTM9b+wSZoO LRhQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:subject:to:cc:references:from:message-id:date :user-agent:mime-version:in-reply-to:content-language :content-transfer-encoding; bh=RTa6LzR7yxsEYxaWCFwuj3D76Cj2BL9uoiJQj/q480g=; b=cpvLlMgjBon3H3dBWEpnmZ31z1Dp4yJ+/DtdfjxlJI31fy1rFCxIU2SqvT+Sml48CH /y5IxD5E28eaW8A5vGgncFyWKih5zHVVaninWy5YakoGe4o48I7ST35F1KnOu76PPZPH CjPMM51Ud0iIEJgp0RZ753ArAjpuUs5wWlbnO2YrIV1ZLQQN48NFh/gTRZkItayIWbkp F+PpB0MmodzfqnjhvkHkFhMUEgQrdkYIozY/P2tm3pFISBIOu7cXZ7E1udv50jsEyoB1 OjV+0eS38evHfpzIZ3M1BiveJzuIt8tgy2heUFAGrpX/PBQyIVNE2XdccRoN27IQKUX9 nmGw== X-Gm-Message-State: AHQUAubwVD7FtAyisrPI45Jc6G4yRQb09btKj5v5gKshuaZWXp69zdNi F+wVrJ86qPutvfpwI5VzqyJP2usp X-Google-Smtp-Source: AHgI3IaBBXddBCkLqqrM04bDlsSQsjlkBEeLfMb0IMaXexKklQyiwQnH+xbAfD1xp46PwJ7ibkfO+A== X-Received: by 2002:a17:902:8d94:: with SMTP id v20mr24695128plo.194.1549661818171; Fri, 08 Feb 2019 13:36:58 -0800 (PST) Received: from tomato.housegordon.com (moose.housegordon.com. [184.68.105.38]) by smtp.googlemail.com with ESMTPSA id z127sm4479066pfb.80.2019.02.08.13.36.56 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 08 Feb 2019 13:36:57 -0800 (PST) Subject: Re: bug#34220: failure to building with CompCert, patch proposed To: Paul Eggert , DAVID MONNIAUX References: <623048061.4346963.1548604407813.JavaMail.zimbra@univ-grenoble-alpes.fr> <41c2e15f-ba21-3307-d9d7-facc3cbe99b5@cs.ucla.edu> From: Assaf Gordon Message-ID: Date: Fri, 8 Feb 2019 14:36:55 -0700 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.4.0 MIME-Version: 1.0 In-Reply-To: <41c2e15f-ba21-3307-d9d7-facc3cbe99b5@cs.ucla.edu> Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: en-US Content-Transfer-Encoding: 7bit X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 34220 Cc: 34220@debbugs.gnu.org, =?UTF-8?Q?P=c3=a1draig_Brady?= X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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 From unknown Fri Jun 20 07:22:19 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Sat, 09 Mar 2019 12:24:04 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator