Your message dated Thu, 01 Aug 2024 21:21:18 +0000
with message-id <[email protected]>
and subject line Bug#1070441: fixed in cbmc 6.1.1-1
has caused the Debian Bug report #1070441,
regarding cbmc: arm64 FTBFS with glibc 2.38
to be marked as done.
This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.
(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact [email protected]
immediately.)
--
1070441: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1070441
Debian Bug Tracking System
Contact [email protected] with problems
--- Begin Message ---
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
--- End Message ---
--- Begin Message ---
Source: cbmc
Source-Version: 6.1.1-1
Done: Michael Tautschnig <[email protected]>
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 [email protected],
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Michael Tautschnig <[email protected]> (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 [email protected])
-----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 <[email protected]>
Changed-By: Michael Tautschnig <[email protected]>
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-----
pgpdtebhbqlnh.pgp
Description: PGP signature
--- End Message ---
