Skip to content

Commit a373657

Browse files
authored
Merge pull request #7843 from tautschnig/bugfixes/__float128
Fix __float128 portability
2 parents 4e426d3 + afb6b2e commit a373657

File tree

4 files changed

+21
-4
lines changed

4 files changed

+21
-4
lines changed

regression/ansi-c/gcc_version1/gcc-5.c

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,5 +9,9 @@ typedef long double _Float128;
99
typedef long double _Float128x;
1010

1111
// But this type should:
12+
// https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
13+
# if defined(__i386__) || defined(__x86_64__) || defined(__ia64__) || \
14+
defined(__hppa__) || defined(__powerpc__)
1215
__float128 f128;
1316
#endif
17+
#endif

regression/ansi-c/gcc_version1/gcc-7.c

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,5 +8,9 @@ _Float64x f64x;
88
_Float128 f128;
99
_Float128x f128x;
1010

11+
// https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
12+
# if defined(__i386__) || defined(__x86_64__) || defined(__ia64__) || \
13+
defined(__hppa__) || defined(__powerpc__)
1114
__float128 gcc_f128;
1215
#endif
16+
#endif

regression/cbmc/ts18661_typedefs/main.c

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,11 @@
1919
# endif
2020

2121
# if __GNUC_PREREQ(4, FLOAT128_MINOR_VERSION)
22-
# define HAS_FLOAT128
22+
// https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
23+
# if defined(__i386__) || defined(__x86_64__) || defined(__ia64__) || \
24+
defined(__hppa__) || defined(__powerpc__)
25+
# define HAS_FLOAT128
26+
# endif
2327
# endif
2428

2529
# endif

src/cpp/cpp_internal_additions.cpp

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -111,9 +111,8 @@ void cpp_internal_additions(std::ostream &out)
111111

112112
if(
113113
config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
114-
config.ansi_c.arch == "x32" || config.ansi_c.arch == "powerpc" ||
115-
config.ansi_c.arch == "ppc64" || config.ansi_c.arch == "ppc64le" ||
116-
config.ansi_c.arch == "ia64")
114+
config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64" ||
115+
config.ansi_c.arch == "powerpc" || config.ansi_c.arch == "ppc64")
117116
{
118117
// https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
119118
// For clang, __float128 is a keyword.
@@ -131,6 +130,12 @@ void cpp_internal_additions(std::ostream &out)
131130
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
132131
out << "typedef long double __float128;" << '\n';
133132
}
133+
else if(config.ansi_c.arch == "ppc64le")
134+
{
135+
// https://patchwork.ozlabs.org/patch/792295/
136+
if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
137+
out << "typedef " CPROVER_PREFIX "Float128 __ieee128;\n";
138+
}
134139

135140
if(
136141
config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||

0 commit comments

Comments
 (0)