Skip to content

Commit df5c550

Browse files
smowtonDaniel Kroening
authored and
Daniel Kroening
committed
Extend cbmc ts18661 test
This now expects to find _Float128 when gcc-4.3+ (x86-64) for -4.5+ (other targets) is in use.
1 parent 3fcd85a commit df5c550

File tree

1 file changed

+17
-3
lines changed
  • regression/cbmc/ts18661_typedefs

1 file changed

+17
-3
lines changed
Lines changed: 17 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,32 @@
1-
#if defined(__clang__)
2-
#elif defined(__GNUC__)
1+
#if defined(__GNUC__) && !defined(__clang__)
2+
3+
#include <features.h> // For __GNUC_PREREQ
4+
5+
#ifdef __x86_64__
6+
#define FLOAT128_MINOR_VERSION 3
7+
#else
8+
#define FLOAT128_MINOR_VERSION 5
9+
#endif
10+
311
#if __GNUC__ >= 7
412
#define HAS_FLOATN
13+
#elif __GNUC_PREREQ(4, FLOAT128_MINOR_VERSION)
14+
#define HAS_FLOAT128
515
#endif
16+
617
#endif
718

819
#ifndef HAS_FLOATN
920
typedef float _Float32;
1021
typedef double _Float32x;
1122
typedef double _Float64;
1223
typedef long double _Float64x;
13-
typedef long double _Float128;
1424
typedef long double _Float128x;
1525
#endif
1626

27+
#if !defined(HAS_FLOATN) && !defined(HAS_FLOAT128)
28+
typedef long double _Float128;
29+
#endif
30+
1731
int main(int argc, char** argv) {
1832
}

0 commit comments

Comments
 (0)