HI Michael,
On 10/14/2014 12:33 PM, Michael Tautschnig wrote: > Many thanks for this patch. It seems upstream has some of these changes in SVN > already and I'll try to merge the missing parts from your patch, but there is > one bit that surprised me a bit in your proposal: Sorry, use this patch, it is better and more complete. Thank you, Breno
--- cbmc-4.9.orig/regression/cbmc/Struct_Bytewise1/struct_bytewise.c +++ cbmc-4.9/regression/cbmc/Struct_Bytewise1/struct_bytewise.c @@ -2,8 +2,8 @@ // Follows http://wiki.debian.org/ArchitectureSpecificsMemo #if defined(__avr32__) || defined(__hppa__) || defined(__mk68k__) || \ - defined(__mips__) || defined(__powerpc__) || defined(__s390__) || \ - defined(__s390x__) || defined(__sparc__) + defined(__mips__) || defined(__s390__) || defined(__s390x__) || \ + defined(__sparc__) || (defined(__powerpc__) && !defined(__LITTLE_ENDIAN__)) #define BIG_ENDIAN --- cbmc-4.9.orig/src/util/config.cpp +++ cbmc-4.9/src/util/config.cpp @@ -339,7 +339,10 @@ void configt::ansi_ct::set_arch_spec_pow set_LP64(); arch=ARCH_POWER; - endianness=IS_BIG_ENDIAN; + if(subarch=="ppc64le") + endianness=IS_LITTLE_ENDIAN; + else + endianness=IS_BIG_ENDIAN; long_double_width=16*8; char_is_unsigned=true; NULL_is_zero=true; @@ -354,6 +357,23 @@ void configt::ansi_ct::set_arch_spec_pow defines.push_back("__ppc__"); if(os==OS_MACOS) defines.push_back("__BIG_ENDIAN__"); + if(subarch!="powerpc") + { + defines.push_back("__powerpc64"); + defines.push_back("__powerpc64__"); + defines.push_back("__PPC64__"); + defines.push_back("__ppc64__"); + if(subarch=="ppc64le") + { + defines.push_back("_CALL_ELF=2"); + defines.push_back("__LITTLE_ENDIAN__"); + } + else + { + defines.push_back("_CALL_ELF=1"); + defines.push_back("__BIG_ENDIAN__"); + } + } break; case MODE_VISUAL_STUDIO_C_CPP: defines.push_back("_M_PPC"); @@ -888,7 +908,8 @@ bool configt::set(const cmdlinet &cmdlin arch=="mips") ansi_c.set_arch_spec_mips(arch); else if(arch=="powerpc" || - arch=="ppc64") + arch=="ppc64" || + arch=="ppc64le") ansi_c.set_arch_spec_power(arch); else if(arch=="sparc") ansi_c.set_arch_spec_sparc(); @@ -1144,10 +1165,14 @@ irep_idt configt::this_architecture() #else this_arch="mips64"; #endif + #elif __ppc64__ || __PPC64__ || __powerpc64__ || __POWERPC64__ + #ifdef __LITTLE_ENDIAN__ + this_arch="ppc64le"; + #else + this_arch="ppc64"; + #endif #elif __powerpc__ this_arch="powerpc"; - #elif __ppc64__ - this_arch="ppc64"; #elif __sparc__ this_arch="sparc"; #elif __ia64__
