Your message dated Wed, 28 Jun 2023 10:51:04 +0000
with message-id <e1qeslm-005wto...@fasolo.debian.org>
and subject line Bug#1038866: fixed in cbmc 5.84.0-10
has caused the Debian Bug report #1038866,
regarding cbmc FTBFS on !x86: Failed test: __asm_fstcw-01
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 ow...@bugs.debian.org
immediately.)
--
1038866: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1038866
Debian Bug Tracking System
Contact ow...@bugs.debian.org with problems
--- Begin Message ---
Source: cbmc
Version: 5.84.0-5
Severity: serious
Tags: ftbfs
https://buildd.debian.org/status/logs.php?pkg=cbmc&ver=5.84.0-5
(m68k builds with nocheck)
...
[31mTests failed[0m
1 of 453 tests failed, 350 tests skipped
Failed test: __asm_fstcw-01
CBMC version 5.84.0 (cbmc-5.76.1) 64-bit arm64 linux
Parsing msvc.i
Converting
Type-checking msvc
Generating GOTO Program
Adding CPROVER library (x86_64)
gcc: error: unrecognized command-line option ‘-m64’
GCC preprocessing failed
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
**** WARNING: no body for function __asm_fstcw
Runtime Symex: 0.0018543s
size of program expression: 32 steps
simple slicing removed 7 assignments
Generated 2 VCC(s), 2 remaining after simplification
Runtime Postprocess Equation: 2.5e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000565307s
Running propositional reduction
Post-processing
Runtime Post-process: 9.22e-06s
Solving with MiniSAT 2.2.1 with simplifier
148 variables, 138 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000284463s
Runtime decision procedure: 0.000977351s
** Results:
msvc.i function main
[main.assertion.1] line 5 default rounding mode: FAILURE
[main.assertion.2] line 9 round upwards: FAILURE
** 2 of 2 failed (2 iterations)
VERIFICATION FAILED
EXIT=10
SIGNAL=0
Failed msvc.desc lines:
^EXIT=0$ [FAILED]
^VERIFICATION SUCCESSFUL$ [FAILED]
make[4]: *** [Makefile:12: test] Error 1
--- End Message ---
--- Begin Message ---
Source: cbmc
Source-Version: 5.84.0-10
Done: Michael Tautschnig <m...@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 1038...@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Michael Tautschnig <m...@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 ftpmas...@ftp-master.debian.org)
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256
Format: 1.8
Date: Wed, 28 Jun 2023 11:27:44 +0100
Source: cbmc
Architecture: source
Version: 5.84.0-10
Distribution: unstable
Urgency: low
Maintainer: Michael Tautschnig <m...@debian.org>
Changed-By: Michael Tautschnig <m...@debian.org>
Closes: 1038866
Changes:
cbmc (5.84.0-10) unstable; urgency=low
.
* Fix more portability problems (Closes: #1038866)
Checksums-Sha1:
260f1353d14720ba6ba663d13382f3280ea39619 2961 cbmc_5.84.0-10.dsc
2c8e7bcdc966abc7949f8991266e497d16ad20a9 57520 cbmc_5.84.0-10.debian.tar.xz
Checksums-Sha256:
6042abe4735dc9aa86bcdcf87b8a72eff856907f803e476b92245a8dfa7572d4 2961
cbmc_5.84.0-10.dsc
147383382343868df8bbfdb15e18567e08fbb4ddbaa34a7f8f643fb313420a3e 57520
cbmc_5.84.0-10.debian.tar.xz
Files:
81f946388254190cf015c403b0acc4ca 2961 science optional cbmc_5.84.0-10.dsc
be3b1c59eceb774bf5f2296d4c791a3b 57520 science optional
cbmc_5.84.0-10.debian.tar.xz
-----BEGIN PGP SIGNATURE-----
Comment: GPGTools - http://gpgtools.org
iQJCBAEBCAAsFiEErKbD9OEAOYbzU4gEO7+DkzbsqTEFAmScDBkOHG10QGRlYmlh
bi5vcmcACgkQO7+DkzbsqTE/2Q//Si2Ue21dNLGquTXjoUHu2Ly6AFRreQXCKUIh
U4NI9VA4U9ucUdOcSQB6VceefhyuDn91oifuge70bd4WtTOYAkwIiFSYzS7iQvme
e3YitnbSKayZ57saskDqnhJN9wPKFTaG3TJfm90Y2m0ztO4JkmUy10NJ5XFiVyfB
8K5TuFRaOkTgqNDG7gkClCiodMtuwCP1ytm6ozIlqDQVGEiScUcn2B2KjzGR6blG
tHM5FDiz3XtKjn80Lj12YVpWxeLvWd37pkGRhf1gaF1WiHBiJ+KIRhPgltwQORPW
H//vv8VqefdglOtxlyOrr8CgPSwpXxu4eLEjQJRzrDcnpsVf/tTQfBREYZ6bUhIk
YhQJ0YWtOzZ0v+/Alzhsa7E8OKNIZCGfiSBTAitNfdzEIX/r84Xy7I+VzIgJkMBj
O7LgfRLRWyB7TTEcAWlUT1bEqT2FdR5rrGmlBFprcQmVQeJdM2Rug2m3A/tfcu4r
HANEwQq9NiO0JPpofn1tI+B/yQhTeQ7uLVmWX0i4uVHMWDXzJ5v7/ae3lESy3zyi
2z1PSvEKT29zcwU9tlY16XZ6dt4gD55ih+bcT4LIs1gOvA7pcYmh1vvmroEQO9mR
MWKVWl4aZqSAavII4pRFIji38fJU7dMsfWhBgjyBvrNR8Kng0OauaXA+STWkZ8SI
6D+fQN4=
=2D3N
-----END PGP SIGNATURE-----
--- End Message ---
