Skip to content

Commit 0dad4fd

Browse files
author
Daniel Kroening
committed
_FloatX support based on gcc version
1 parent 298ec01 commit 0dad4fd

File tree

9 files changed

+38
-21
lines changed

9 files changed

+38
-21
lines changed

‎regression/ansi-c/float_constant1/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ STATIC_ASSERT(0X.0p+1f == 0);
1212

1313
// 32-bit, 64-bit and 128-bit constants, GCC proper only,
1414
// clang doesn't have it
15-
#if defined(__GNUC__) && !defined(__clang__)
15+
#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ >= 7
1616
STATIC_ASSERT(__builtin_types_compatible_p(_Float32, __typeof(1.0f32)));
1717
STATIC_ASSERT(__builtin_types_compatible_p(_Float64, __typeof(1.0f64)));
1818
STATIC_ASSERT(__builtin_types_compatible_p(_Float128, __typeof(1.0f128)));

‎regression/ansi-c/gcc_types_compatible_p1/main.c

+6-3
Original file line numberDiff line numberDiff line change
@@ -67,8 +67,8 @@ STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot) *, int *));
6767
STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot), typeof (janette)));
6868
STATIC_ASSERT(__builtin_types_compatible_p(__int128, signed __int128));
6969

70-
#ifndef __clang__
7170
// clang doesn't have these
71+
#if !defined(__clang__) && __GNUC__ >= 7
7272
#if defined(__x86_64__) || defined(__i386__)
7373
STATIC_ASSERT(__builtin_types_compatible_p(__float128, _Float128));
7474
#endif
@@ -95,16 +95,19 @@ STATIC_ASSERT(!__builtin_types_compatible_p(long int, int));
9595
STATIC_ASSERT(!__builtin_types_compatible_p(long long int, long int));
9696
STATIC_ASSERT(!__builtin_types_compatible_p(unsigned, signed));
9797

98-
#ifndef __clang__
98+
STATIC_ASSERT(!__builtin_types_compatible_p(__int128, unsigned __int128));
99+
99100
// clang doesn't have these
101+
#if !defined(__clang__)
102+
#if __GNUC__ >= 7
100103
STATIC_ASSERT(!__builtin_types_compatible_p(_Float32, float));
101104
STATIC_ASSERT(!__builtin_types_compatible_p(_Float64, double));
102105
STATIC_ASSERT(!__builtin_types_compatible_p(_Float32x, float));
103106
STATIC_ASSERT(!__builtin_types_compatible_p(_Float64x, double));
107+
#endif
104108
STATIC_ASSERT(!__builtin_types_compatible_p(__float80, double));
105109
STATIC_ASSERT(!__builtin_types_compatible_p(__float128, long double));
106110
STATIC_ASSERT(!__builtin_types_compatible_p(__float128, double));
107-
STATIC_ASSERT(!__builtin_types_compatible_p(__int128, unsigned __int128));
108111
#endif
109112
#endif
110113

‎src/ansi-c/ansi_c_language.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,7 @@ bool ansi_c_languaget::parse(
7575
ansi_c_parser.in=&codestr;
7676
ansi_c_parser.set_message_handler(get_message_handler());
7777
ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
78+
ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
7879
ansi_c_parser.cpp98=false; // it's not C++
7980
ansi_c_parser.cpp11=false; // it's not C++
8081
ansi_c_parser.mode=config.ansi_c.mode;
@@ -196,6 +197,7 @@ bool ansi_c_languaget::to_expr(
196197
ansi_c_parser.in=&i_preprocessed;
197198
ansi_c_parser.set_message_handler(get_message_handler());
198199
ansi_c_parser.mode=config.ansi_c.mode;
200+
ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
199201
ansi_c_scanner_init();
200202

201203
bool result=ansi_c_parser.parse();

‎src/ansi-c/ansi_c_parser.h

+5-1
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,8 @@ class ansi_c_parsert:public parsert
3535
mode(modet::NONE),
3636
cpp98(false),
3737
cpp11(false),
38-
for_has_scope(false)
38+
for_has_scope(false),
39+
ts_18661_3_Floatn_types(false)
3940
{
4041
}
4142

@@ -77,6 +78,9 @@ class ansi_c_parsert:public parsert
7778
// in C99 and upwards, for(;;) has a scope
7879
bool for_has_scope;
7980

81+
// ISO/IEC TS 18661-3:2015
82+
bool ts_18661_3_Floatn_types;
83+
8084
typedef ansi_c_identifiert identifiert;
8185
typedef ansi_c_scopet scopet;
8286

‎src/ansi-c/scanner.l

+13-14
Original file line numberDiff line numberDiff line change
@@ -459,36 +459,31 @@ void ansi_c_scanner_init()
459459
return make_identifier();
460460
}
461461

462-
"_Float16" { // clang doesn't have it
463-
if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
462+
"_Float16" { if(PARSER.ts_18661_3_Floatn_types)
464463
{ loc(); return TOK_GCC_FLOAT16; }
465464
else
466465
return make_identifier();
467466
}
468467

469-
"_Float32" { // clang doesn't have it
470-
if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
468+
"_Float32" { if(PARSER.ts_18661_3_Floatn_types)
471469
{ loc(); return TOK_GCC_FLOAT32; }
472470
else
473471
return make_identifier();
474472
}
475473

476-
"_Float32x" { // clang doesn't have it
477-
if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
474+
"_Float32x" { if(PARSER.ts_18661_3_Floatn_types)
478475
{ loc(); return TOK_GCC_FLOAT32X; }
479476
else
480477
return make_identifier();
481478
}
482479

483-
"_Float64" { // clang doesn't have it
484-
if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
480+
"_Float64" { if(PARSER.ts_18661_3_Floatn_types)
485481
{ loc(); return TOK_GCC_FLOAT64; }
486482
else
487483
return make_identifier();
488484
}
489485

490-
"_Float64x" { // clang doesn't have it
491-
if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
486+
"_Float64x" { if(PARSER.ts_18661_3_Floatn_types)
492487
{ loc(); return TOK_GCC_FLOAT64X; }
493488
else
494489
return make_identifier();
@@ -501,16 +496,20 @@ void ansi_c_scanner_init()
501496
return make_identifier();
502497
}
503498

504-
"__float128" |
505-
"_Float128" { // clang doesn't have it
499+
"__float128" { // clang doesn't have it
506500
if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
507501
{ loc(); return TOK_GCC_FLOAT128; }
508502
else
509503
return make_identifier();
510504
}
511505

512-
"_Float128x" { // clang doesn't have it
513-
if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
506+
"_Float128" { if(PARSER.ts_18661_3_Floatn_types)
507+
{ loc(); return TOK_GCC_FLOAT128; }
508+
else
509+
return make_identifier();
510+
}
511+
512+
"_Float128x" { if(PARSER.ts_18661_3_Floatn_types)
514513
{ loc(); return TOK_GCC_FLOAT128X; }
515514
else
516515
return make_identifier();

‎src/cpp/cpp_parser.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ bool cpp_parsert::parse()
2424
ansi_c_parser.cpp11=
2525
config.cpp.cpp_standard==configt::cppt::cpp_standardt::CPP11 ||
2626
config.cpp.cpp_standard==configt::cppt::cpp_standardt::CPP14;
27+
ansi_c_parser.ts_18661_3_Floatn_types=false;
2728
ansi_c_parser.in=in;
2829
ansi_c_parser.mode=mode;
2930
ansi_c_parser.set_file(get_file());

‎src/goto-cc/gcc_mode.cpp

+5
Original file line numberDiff line numberDiff line change
@@ -525,6 +525,11 @@ int gcc_modet::doit()
525525
if(cmdline.isset("-fsingle-precision-constant"))
526526
config.ansi_c.single_precision_constant=true;
527527

528+
// ISO/IEC TS 18661-3:2015 support was introduced with gcc 7.0
529+
if(gcc_version.flavor==gcc_versiont::flavort::GCC &&
530+
gcc_version.is_at_least(7))
531+
config.ansi_c.ts_18661_3_Floatn_types=true;
532+
528533
// -fshort-double makes double the same as float
529534
if(cmdline.isset("fshort-double"))
530535
config.ansi_c.double_width=config.ansi_c.single_width;

‎src/util/config.cpp

+4-2
Original file line numberDiff line numberDiff line change
@@ -738,6 +738,7 @@ bool configt::set(const cmdlinet &cmdline)
738738

739739
ansi_c.single_precision_constant=false;
740740
ansi_c.for_has_scope=true; // C99 or later
741+
ansi_c.ts_18661_3_Floatn_types=false;
741742
ansi_c.c_standard=ansi_ct::default_c_standard();
742743
ansi_c.endianness=ansi_ct::endiannesst::NO_ENDIANNESS;
743744
ansi_c.os=ansi_ct::ost::NO_OS;
@@ -1135,8 +1136,9 @@ void configt::set_from_symbol_table(
11351136

11361137
ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
11371138
ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
1138-
// for_has_scope, single_precision_constant, rounding_mode not
1139-
// stored in namespace
1139+
// for_has_scope, single_precision_constant, rounding_mode,
1140+
// ts_18661_3_Floatn_types are not architectural features,
1141+
// and thus not stored in namespace
11401142

11411143
ansi_c.alignment=unsigned_from_ns(ns, "alignment");
11421144

‎src/util/config.h

+1
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,7 @@ class configt
4242
// various language options
4343
bool char_is_unsigned, wchar_t_is_unsigned;
4444
bool for_has_scope;
45+
bool ts_18661_3_Floatn_types; // ISO/IEC TS 18661-3:2015
4546
bool single_precision_constant;
4647
enum class c_standardt { C89, C99, C11 } c_standard;
4748
static c_standardt default_c_standard();

0 commit comments

Comments
 (0)