File tree Expand file tree Collapse file tree 4 files changed +21
-4
lines changed
Expand file tree Collapse file tree 4 files changed +21
-4
lines changed Original file line number Diff line number Diff line change @@ -9,5 +9,9 @@ typedef long double _Float128;
99typedef 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
Original file line number Diff line number Diff 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
Original file line number Diff line number Diff line change 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
Original file line number Diff line number Diff 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" ||
You can’t perform that action at this time.
0 commit comments