Debian Bug report logs - #1070441
cbmc: arm64 FTBFS with glibc 2.38

Reply or subscribe to this bug.

Toggle useless messages

Message #5 received at submit@bugs.debian.org (full text, mbox, reply):

From: Graham Inggs <ginggs@debian.org>

To: Debian Bug Tracking System <submit@bugs.debian.org>

Subject: cmbc: arm64 FTBFS with glibc 2.38

Date: Sun, 5 May 2024 11:59:25 +0000

Source: cbmc
Version: 5.95.1-4
Severity: serious
Tags: ftbfs

Hi Maintainer

As can be seen in reproducible builds [1], cbmc FTBFS on arm64 with
glibc 2.38.  I've copied what I hope is the relevant part of the log
below.

A bug was filed against glibc [2], but it seems glibc upstream do not
consider it a bug in glibc.

Regards
Graham


[1] https://tests.reproducible-builds.org/debian/rb-pkg/cbmc.html
[2] https://sourceware.org/bugzilla/show_bug.cgi?id=30909


 [31mTests failed [0m
  10 of 1114 tests failed, 60 tests skipped


Failed test: Float-div2
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux
Parsing main.c
file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax
error before '__f32x4_t'
PARSING ERROR

EXIT=6
SIGNAL=0



Failed test.desc lines:
^EXIT=0$ [FAILED]
^VERIFICATION SUCCESSFUL$ [FAILED]


Failed test: Float-div3
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux
Parsing main.c
file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax
error before '__f32x4_t'
PARSING ERROR

EXIT=6
SIGNAL=0



Failed test.desc lines:
^EXIT=0$ [FAILED]
^VERIFICATION SUCCESSFUL$ [FAILED]


Failed test: Float-equality2
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux
Parsing main.c
file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax
error before '__f32x4_t'
PARSING ERROR

EXIT=6
SIGNAL=0



Failed test.desc lines:
(Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$) [FAILED]
^VERIFICATION SUCCESSFUL$ [FAILED]
^EXIT=0$ [FAILED]


Failed test: Float-flags-no-simp1
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux
Parsing main.c
file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax
error before '__f32x4_t'
PARSING ERROR

EXIT=6
SIGNAL=0



Failed test.desc lines:
^EXIT=0$ [FAILED]
^VERIFICATION SUCCESSFUL$ [FAILED]


Failed test: Float-flags-simp1
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux
Parsing main.c
file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax
error before '__f32x4_t'
PARSING ERROR

EXIT=6
SIGNAL=0



Failed test.desc lines:
^EXIT=0$ [FAILED]
^VERIFICATION SUCCESSFUL$ [FAILED]


Failed test: Float-no-simp9
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux
Parsing main.c
file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax
error before '__f32x4_t'
PARSING ERROR

EXIT=6
SIGNAL=0



Failed test.desc lines:
^EXIT=0$ [FAILED]
^VERIFICATION SUCCESSFUL$ [FAILED]


Failed test: Float21
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux
Parsing main.c
file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax
error before '__f32x4_t'
PARSING ERROR

EXIT=6
SIGNAL=0



Failed test.desc lines:
^EXIT=0$ [FAILED]
^VERIFICATION SUCCESSFUL$ [FAILED]


Failed test: float-nan-check
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux
Parsing main.c
file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax
error before '__f32x4_t'
PARSING ERROR

EXIT=6
SIGNAL=0

Message #10 received at 1070441@bugs.debian.org (full text, mbox, reply):

From: Aurelien Jarno <aurel32@debian.org>

To: 1070441@bugs.debian.org, 1070443@bugs.debian.org, 1070444@bugs.debian.org, 1070446@bugs.debian.org

Cc: debian-glibc@lists.debian.org

Subject: FTBFS due to /usr/include/aarch64-linux-gnu/bits/math-vector.h

Date: Mon, 6 May 2024 23:14:51 +0200

control: severity 1070441 important
control: block 1070668 by 1070441
control: severity 1070443 important
control: block 1070668 by 1070443
control: severity 1070444 important
control: block 1070668 by 1070444
control: severity 1070446 important
control: block 1070668 by 1070446


Dear maintainers,

glibc 2.38 introduced changes to the bits/math-vector.h file on arm64 in
order to support math vector functions. This unfortunately caused the
FTBFS of your packages.

The change has been temporarily reverted in version 2.38-8 until a fix
is found, and I have opened #1070668 on the glibc side to track the
issue, with a Cc: to the arm64 porters.

I am therefore downgrading the bugs to severity important. However this
should not prevent working on a solution to the problem with the arm64
porters, and depending on the case either at the package level, or at
the upstream glibc/gcc/llvm level.

Regards
Aurelien

-- 
Aurelien Jarno                          GPG: 4096R/1DDD8C9B
aurelien@aurel32.net                     http://aurel32.net

Message #25 received at 1070441-close@bugs.debian.org (full text, mbox, reply):

From: Debian FTP Masters <ftpmaster@ftp-master.debian.org>

To: 1070441-close@bugs.debian.org

Subject: Bug#1070441: fixed in cbmc 6.1.1-1

Date: Thu, 01 Aug 2024 21:21:18 +0000

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

Source: cbmc
Source-Version: 6.1.1-1
Done: Michael Tautschnig <mt@debian.org>

We believe that the bug you reported is fixed in the latest version of
cbmc, which is due to be installed in the Debian FTP archive.

A summary of the changes between this version and the previous one is
attached.

Thank you for reporting the bug, which will now be closed.  If you
have further comments please address them to 1070441@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Michael Tautschnig <mt@debian.org> (supplier of updated cbmc package)

(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@ftp-master.debian.org)


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Format: 1.8
Date: Thu, 01 Aug 2024 17:57:12 +0000
Source: cbmc
Binary: cbmc cbmc-dbgsym jbmc jbmc-dbgsym
Architecture: source
Version: 6.1.1-1
Distribution: unstable
Urgency: low
Maintainer: Michael Tautschnig <mt@debian.org>
Changed-By: Michael Tautschnig <mt@debian.org>
Description:
 cbmc       - bounded model checker for C and C++ programs
 jbmc       - bounded model checker for Java programs
Closes: 1070441 1074869
Changes:
 cbmc (6.1.1-1) unstable; urgency=low
 .
   * New upstream release, which includes support for building with GCC 14
     (Closes: #1074869)
   * Support ARM-specific vector types (Closes: #1070441)
Checksums-Sha1:
 3a25a01fdb57525b439a57f774aa86703e61ec3f 3048 cbmc_6.1.1-1.dsc
 18f8cbbe349484a1adf2b8e4cf3a1b4822b97d31 14582 cbmc_6.1.1.orig-java-cprover-api.tar.gz
 ca108e17fc68557cce10a6d5d9d84ab39395d2d6 299209 cbmc_6.1.1.orig-java-models-library.tar.gz
 cde78b4c4f59cc8721c7828fb0db33b6e11fb336 9114649 cbmc_6.1.1.orig.tar.gz
 7182386f067ba0d99dc361a05e66b1392966f87c 17788 cbmc_6.1.1-1.debian.tar.xz
Checksums-Sha256:
 12c0baee24140f3b872269f30c38dd84fc87a93aaa31f9e0c51314b639818caa 3048 cbmc_6.1.1-1.dsc
 70863817bba398e8bb252c96ec1fbe35d20882f9061c920189893080f14646ab 14582 cbmc_6.1.1.orig-java-cprover-api.tar.gz
 13eb3b8513de999d52eb071d7118b147f8511390c3cb30a6c3be29ada3b5b3c9 299209 cbmc_6.1.1.orig-java-models-library.tar.gz
 aec0f781ec4c3b1ebb7ae1a2bb4b4484ee04b33f9a7c66cb913af97dbeb87801 9114649 cbmc_6.1.1.orig.tar.gz
 17c071b9b1d4f797fdfd83b913b7eebbf3c77d834b576520deb9bcd3ec23a54b 17788 cbmc_6.1.1-1.debian.tar.xz
Files:
 9027e0ea6a50a4e68c627afa9b586202 3048 science optional cbmc_6.1.1-1.dsc
 245cc4a092fb84d4c8a1333c793f1adc 14582 science optional cbmc_6.1.1.orig-java-cprover-api.tar.gz
 6ba4b12d1ad0ee6f917128fa61df4015 299209 science optional cbmc_6.1.1.orig-java-models-library.tar.gz
 000c8d5c62a91c8bdd6aaefe7a74e147 9114649 science optional cbmc_6.1.1.orig.tar.gz
 46e2c7e364f4288904363193172648b7 17788 science optional cbmc_6.1.1-1.debian.tar.xz

-----BEGIN PGP SIGNATURE-----

iQJCBAEBCgAsFiEErKbD9OEAOYbzU4gEO7+DkzbsqTEFAmar+CwOHG10QGRlYmlh
bi5vcmcACgkQO7+DkzbsqTHqRg//Q3Q6ePm+QaROXxAe4uTaauHYrrSkjZMZXkUs
lFGCGnBp9kQdinl4Mwhvpi+USgreeTOlxEIiQ6exEcnJGDqsKvsfmtH0fy+aLowr
2Vl/l1KWzzgFhDbSJezxaLbIzq/DwYMpwBgLdG09G36BXBiXqd/Wr+6PCXxIfgTH
fIgiPEhY16Q0DCLmFHeg7LIZIgO11Qx289ZD1yvPWtHxiCNlcL1YSfTAU8+0GnJq
bhsCcp93ZIbB+A7VPP4Y33WIzP3iaAh556p514LxXiJjQQVX+z+DreO7WtHPPk9q
JCiXrcA5leDNKk6ig26L3zrfEvEoVRjG7fwtBbRStl9PhRIqv4maPPI9CVurseo1
TaBLOgO7Ug6JX46fO4jeZBkfifO/teUVZVrdefUncy4t7R7rvx9AH1iEkpV4Dpk8
8CnAGy22QVQNvulyXy1BrKtjHVbrowQh9ltIf+2Dp+tq+N+DTFb4bIV6V+gjpVZl
wdIzotDZEJXRR3hrWNJZCOgl1sw5H0qR1cZyfKylqOBjkYAOJ+TjhDStjn5FlOmw
Dpm2R+BuOkfdQZXmtQYYja/VicaWpcAjVXPTNosHKAvhInvUClZ1khpG38mcnEZD
Sqm+mSFQklsz/0eOjqVMF/OsBsrlTgE+hztxxjXL23i4LZ1FBmyH6VrxQ+RR3WpS
fvOWjdw=
=rQJX
-----END PGP SIGNATURE-----

[Message part 2 (application/pgp-signature, inline)]

Send a report that this bug log contains spam.