Skip to content

Commit 618fb5a

Browse files
committed
Little-endian PowerPC-64 uses __ieee128 instead of __float128
GCC set a macro re-defining __float128 to __ieee128, but just on this one architecture. See https://buildd.debian.org/status/logs.php?pkg=cbmc&arch=ppc64el, https://buildd.debian.org/status/logs.php?pkg=cbmc&arch=ppc64, https://buildd.debian.org/status/logs.php?pkg=cbmc&arch=powerpc, with the build logs for 5.10-2 vs. 5.10-3.
1 parent 8401f49 commit 618fb5a

File tree

1 file changed

+8
-3
lines changed

1 file changed

+8
-3
lines changed

src/ansi-c/ansi_c_internal_additions.cpp

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -194,16 +194,21 @@ void ansi_c_internal_additions(std::string &code)
194194

195195
if(
196196
config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
197-
config.ansi_c.arch == "x32" || config.ansi_c.arch == "powerpc" ||
198-
config.ansi_c.arch == "ppc64" || config.ansi_c.arch == "ppc64le" ||
199-
config.ansi_c.arch == "ia64")
197+
config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64" ||
198+
config.ansi_c.arch == "powerpc" || config.ansi_c.arch == "ppc64")
200199
{
201200
// https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
202201
// For clang, __float128 is a keyword.
203202
// For gcc, this is a typedef and not a keyword.
204203
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
205204
code += "typedef __CPROVER_Float128 __float128;\n";
206205
}
206+
else if(config.ansi_c.arch == "ppc64le")
207+
{
208+
// https://patchwork.ozlabs.org/patch/792295/
209+
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
210+
code += "typedef __CPROVER_Float128 __ieee128;\n";
211+
}
207212
else if(config.ansi_c.arch == "hppa")
208213
{
209214
// https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html

0 commit comments

Comments
 (0)