Your message dated Sun, 04 Dec 2016 11:48:30 +0000
with message-id <e1cdvhs-0007zx...@fasolo.debian.org>
and subject line Bug#844776: fixed in cbmc 5.6-1
has caused the Debian Bug report #844776,
regarding cbmc FTBFS on s390x and mips*: Running Pointer_array5/test.desc FAILED
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.)
--
844776: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=844776
Debian Bug Tracking System
Contact ow...@bugs.debian.org with problems
--- Begin Message ---
Source: cbmc
Version: 5.5-1
Severity: serious
https://buildd.debian.org/status/package.php?p=cbmc&suite=sid
...
Running Pointer_array5/test.desc [FAILED]
...
Tests failed
1 of 383 tests failed, 20 tests skipped
Failed test: Pointer_array5
CBMC version 5.5 64-bit s390x linux
Parsing main.c
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__"
redefined
<built-in>: note: this is the location of the previous definition
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (s390x)
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__"
redefined
<built-in>: note: this is the location of the previous definition
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 95 steps
simple slicing removed 24 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
12568 variables, 25409 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.114s
** Results:
[main.assertion.1] assertion address==&a0: FAILURE
** 1 of 1 failed (1 iteration)
VERIFICATION FAILED
EXIT=10
SIGNAL=0
debian/rules:31: recipe for target 'override_dh_auto_test' failed
make[1]: *** [override_dh_auto_test] Error 1
make[1]: Leaving directory '/«PKGBUILDDIR»'
debian/rules:15: recipe for target 'build-arch' failed
make: *** [build-arch] Error 2
dpkg-buildpackage: error: debian/rules build-arch gave error exit status 2
--- End Message ---
--- Begin Message ---
Source: cbmc
Source-Version: 5.6-1
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 844...@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: Sun, 04 Dec 2016 09:18:48 +0000
Source: cbmc
Binary: cbmc
Architecture: source i386
Version: 5.6-1
Distribution: unstable
Urgency: low
Maintainer: Michael Tautschnig <m...@debian.org>
Changed-By: Michael Tautschnig <m...@debian.org>
Description:
cbmc - bounded model checker for C and C++ programs
Closes: 844776
Changes:
cbmc (5.6-1) unstable; urgency=low
.
* New upstream release
* Disable Pointer_array5 test due to endianness bugs (Closes: #844776)
Checksums-Sha1:
755eb15e1bc8fc9365a0f30ebd2d0d40e5f70f95 1744 cbmc_5.6-1.dsc
d2beb6e29e66bb1069b3dbbc702b15fb59a96568 5459880 cbmc_5.6.orig.tar.gz
4a92c2c4432642f43e9f43bc4d2b1b6372694ecf 10608 cbmc_5.6-1.debian.tar.xz
Checksums-Sha256:
11b3090d64950e9e715fc8d5afd2c08c0e4d81c034aaf671301b6842d7635244 1744
cbmc_5.6-1.dsc
c6bef63ec42816d0add995ea3b2a5344845cc31f0a6b9e4b8a18df8bb8ad904f 5459880
cbmc_5.6.orig.tar.gz
0d6c4d776f662dc82a70ed16c411446ffe4d9e1de514966abec4c0482d46627c 10608
cbmc_5.6-1.debian.tar.xz
Files:
8fc578de2f81896178a6b6f816414bbc 1744 science extra cbmc_5.6-1.dsc
37d634b10b16dae52fc80436aa046818 5459880 science extra cbmc_5.6.orig.tar.gz
0a31bdd2649de3f0bb427a45b1146706 10608 science extra cbmc_5.6-1.debian.tar.xz
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1
Comment: GPGTools - http://gpgtools.org
iQIcBAEBCAAGBQJYQ/+jAAoJEDu/g5M27KkxE44P/0kYFcGxl+hcf4FZImxKcbDD
Vs6EKfrLHPF7vCKI+E/V3aT5ncnGjdIFTt53E0so7u74R5N9N4e5HhxTyn7Ol4+T
5RRLN2TNA+OTIX8t92dOe7FUvbzSYxGRwkxxhDBg8kSbk1/WPfSBSmO9L9kE/W4d
TQS69N8ZKI93YJCtmdU4TZr8lnxEvS9BUslGuwMNwQAbQEdXnSmu4CZ4SuxorOGR
KdI6c5PNvDyEDO5pb2jETcAddXfiCc0wJXv8JOYUGhY4p18aYtacSxihg6YNsu92
x5cMMpCf8SRnbT05fQupeymxqiRargrmx7JfRsRxzPT0BVyIul/dE/8Hv/dFYweh
MeD6B62saTFI1xaWSnIGP8XNYl/K3LVPjjxkItskdUS1BDJPELn4/7ID61PhKZWt
Kw4pBfLhnZquCl2NRMchW5ITMWEmY7EiMtbc2yJOBUvW+y7yRb3XUJzzP9eOHOlK
JxTF8y2tuQx4jSEBIv9pavjiUaF9lICn07j1NYKgq4J2rmdgyps9gXpU1b4VwcLQ
k8f7CrbcguF5aQCWNs4XvfoHmnaUf0WRMdwerCE5lFPBiKdyDf4JfSpFg15biXjR
M3TPQGKMyxr7mHiyaYDX+8zv+zHqsl24tfncO7wee5rZBJfbocpqMlPvsXRUemZE
XKP145C84DZx6rvYfrtJ
=XP7I
-----END PGP SIGNATURE-----
--- End Message ---
