Your message dated Thu, 29 Jan 2015 09:19:10 +0000
with message-id <[email protected]>
and subject line Bug#765376: fixed in cbmc 5.0-1
has caused the Debian Bug report #765376,
regarding Add initial support for ppc64el
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.)
--
765376: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=765376
Debian Bug Tracking System
Contact [email protected] with problems
--- Begin Message ---
Package: cbmc
Version: 4.9.4-4
Severity: normal
Tags: patch
This patch adds initial support for ppc64el, fixing a lot of test failures that
is happening on buildd right now.
Thank you,
Breno
+--- src/util/config.cpp
++++ src/util/config.cpp
+@@ -336,8 +336,12 @@ void configt::ansi_ct::set_arch_spec_pow
+ else // ppc64
+ set_LP64();
+
++ if(subarch=="ppc64le")
++ endianness=IS_LITTLE_ENDIAN;
++ else
++ endianness=IS_BIG_ENDIAN;
++
+ arch=ARCH_POWER;
+- endianness=IS_BIG_ENDIAN;
+ long_double_width=16*8;
+ char_is_unsigned=true;
+
+@@ -345,10 +349,13 @@ void configt::ansi_ct::set_arch_spec_pow
+ {
+ case MODE_GCC_C:
+ case MODE_GCC_CPP:
+- defines.push_back("__powerpc");
+- defines.push_back("__powerpc__");
+- defines.push_back("__POWERPC__");
+- defines.push_back("__ppc__");
++ if(subarch=="powerpc")
++ {
++ defines.push_back("__powerpc");
++ defines.push_back("__powerpc__");
++ defines.push_back("__POWERPC__");
++ defines.push_back("__ppc__");
++ }
+ if(os==OS_MACOS)
+ defines.push_back("__BIG_ENDIAN__");
+ break;
+@@ -1072,9 +1079,15 @@ irep_idt configt::this_architecture()
+ #elif __mips__
+ this_arch="mips";
+ #elif __powerpc__
+- this_arch="powerpc";
+- #elif __ppc64__
+- this_arch="ppc64";
++ #if defined(__ppc64__) || defined(__PPC64__) || defined(__powerpc64__) ||
defined(__POWERPC64__)
++ #ifdef __LITTLE_ENDIAN__
++ this_arch="ppc64le";
++ #else
++ this_arch="ppc64";
++ #endif
++ #else
++ this_arch="powerpc";
++ #endif
+ #elif __sparc__
+ this_arch="sparc";
+ #elif __ia64__
+
--- cbmc-4.9.orig/src/util/config.cpp
+++ cbmc-4.9/src/util/config.cpp
@@ -338,8 +338,12 @@ void configt::ansi_ct::set_arch_spec_pow
else // ppc64
set_LP64();
+ if(subarch=="ppc64le")
+ endianness=IS_LITTLE_ENDIAN;
+ else
+ endianness=IS_BIG_ENDIAN;
+
arch=ARCH_POWER;
- endianness=IS_BIG_ENDIAN;
long_double_width=16*8;
char_is_unsigned=true;
NULL_is_zero=true;
@@ -348,10 +352,13 @@ void configt::ansi_ct::set_arch_spec_pow
{
case MODE_GCC_C:
case MODE_GCC_CPP:
- defines.push_back("__powerpc");
- defines.push_back("__powerpc__");
- defines.push_back("__POWERPC__");
- defines.push_back("__ppc__");
+ if(subarch=="powerpc")
+ {
+ defines.push_back("__powerpc");
+ defines.push_back("__powerpc__");
+ defines.push_back("__POWERPC__");
+ defines.push_back("__ppc__");
+ }
if(os==OS_MACOS)
defines.push_back("__BIG_ENDIAN__");
break;
@@ -1145,9 +1152,15 @@ irep_idt configt::this_architecture()
this_arch="mips64";
#endif
#elif __powerpc__
- this_arch="powerpc";
- #elif __ppc64__
- this_arch="ppc64";
+ #if defined(__ppc64__) || defined(__PPC64__) || defined(__powerpc64__) ||
defined(__POWERPC64__)
+ #ifdef __LITTLE_ENDIAN__
+ this_arch="ppc64le";
+ #else
+ this_arch="ppc64";
+ #endif
+ #else
+ this_arch="powerpc";
+ #endif
#elif __sparc__
this_arch="sparc";
#elif __ia64__
--- End Message ---
--- Begin Message ---
Source: cbmc
Source-Version: 5.0-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 [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: SHA256
Format: 1.8
Date: Thu, 29 Jan 2015 07:30:49 +0000
Source: cbmc
Binary: cbmc
Architecture: source i386
Version: 5.0-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
Closes: 765376
Changes:
cbmc (5.0-1) unstable; urgency=low
.
* New upstream release
* Most 4.9 patches merged
* Includes support for ppc64el. Thanks Breno Leitao for further patches.
(Closes: #765376)
Checksums-Sha1:
337da1d4e94686e715ae1caf7799e6ee98cb5166 1746 cbmc_5.0-1.dsc
27109c8d352418eb92c32c4ef78492c43a926e93 5088984 cbmc_5.0.orig.tar.gz
4846921042b43a815c89263ef93778816c97f527 9836 cbmc_5.0-1.debian.tar.xz
Checksums-Sha256:
26ed943a2f8cd0fbec46c32a7391a4fee5c3abbccdcfad9f163d7ae7e450ec17 1746
cbmc_5.0-1.dsc
667cc36ac0c059fa9dae6a1b3df5c76725842d8bd4218d3c93080c7f47c357c1 5088984
cbmc_5.0.orig.tar.gz
e59f66460f1ff99d43a33cbfeaf658988aaa7e8d95d508685d9eeeb212aafb81 9836
cbmc_5.0-1.debian.tar.xz
Files:
dd1dd1e60d1b13468e5cb1a877269c32 1746 science extra cbmc_5.0-1.dsc
7f78627c7dd5d3f38a804003f6c53aa6 5088984 science extra cbmc_5.0.orig.tar.gz
3f74a7b9be2281eec2419a14d0f4acc2 9836 science extra cbmc_5.0-1.debian.tar.xz
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.12 (GNU/Linux)
Comment: GPGTools - http://gpgtools.org
iQIcBAEBCAAGBQJUyeyzAAoJEDu/g5M27KkxzIQP/RI/SjQOoNnd0+Rmg8f0qyCM
cN0h3ZHNZcF2nSvm9xGyMr0ZwWo9/vG2xs+rK9FScGm18UnacrON4M+wnozjSHR0
2BQSTPeESb9zfarUs15ThCGIZjXIr0Q6Z/3BU7t3g4HzrMNFBmMeqIHaRdAgndrJ
LBi09KCkVyKUvZYjUuso58vPoFpePTJTvEBeV7mmwtuCmcaEz9sSabLw8SqGL5nV
UuPXx78y1DlbsimncEgwr+BEiLy27GqEe4tmnE5uXGbaOSyR2mC8mjav9fQWFAdH
gVhh3l3S+iP8zz3E3ebZoYkbRiaufi3CmalxJrMgIRfBGaJ29XPugisBeRGDGXcP
+fAiH75c3VDCcwsZX3qaeaVm0lun2uVMnDfr5LM13m9cyptl7wmXBlx4rNQKk+tJ
WFP/dCEjrY935Adza0vhiZQC/78GZAwkvTiGHbx7gGBAQdki+TbYIMYYEFVfA5jw
mPVHjeb6BAc1XVXNme1FYMHnGcRD4Sm4cxQimYjyGkMw9T1HY1WfqrXyR+5ETC29
u0qWVqOvQ7nJtnHqHsK4tKxt7mmHOzPl6I1zJjEwLarBFJz5ZEbS7NBVF+6Ud7OG
BYR4N84MOm+trWYp02fFWqGooYmU7DwwCZH/YpzZZ5r0gUacJUSfmOc5WSyUDMBp
gC3nt/Ch9GO+dyIt/zps
=iBSV
-----END PGP SIGNATURE-----
--- End Message ---
