diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index 5c58cf621a7..6e83d9e592f 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -78,6 +78,7 @@ bool ansi_c_languaget::parse( ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types; ansi_c_parser.float16_type = config.ansi_c.float16_type; ansi_c_parser.bf16_type = config.ansi_c.bf16_type; + ansi_c_parser.fp16_type = config.ansi_c.fp16_type; ansi_c_parser.cpp98=false; // it's not C++ ansi_c_parser.cpp11=false; // it's not C++ ansi_c_parser.mode=config.ansi_c.mode; @@ -202,6 +203,7 @@ bool ansi_c_languaget::to_expr( ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types; ansi_c_parser.float16_type = config.ansi_c.float16_type; ansi_c_parser.bf16_type = config.ansi_c.bf16_type; + ansi_c_parser.fp16_type = config.ansi_c.fp16_type; ansi_c_parser.cpp98 = false; // it's not C++ ansi_c_parser.cpp11 = false; // it's not C++ ansi_c_parser.mode = config.ansi_c.mode; diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h index b459b1ba4ce..206e7be8dda 100644 --- a/src/ansi-c/ansi_c_parser.h +++ b/src/ansi-c/ansi_c_parser.h @@ -37,7 +37,8 @@ class ansi_c_parsert:public parsert for_has_scope(false), ts_18661_3_Floatn_types(false), float16_type(false), - bf16_type(false) + bf16_type(false), + fp16_type(false) { // set up global scope scopes.clear(); @@ -69,6 +70,7 @@ class ansi_c_parsert:public parsert bool ts_18661_3_Floatn_types; bool float16_type; bool bf16_type; + bool fp16_type; typedef ansi_c_identifiert identifiert; typedef ansi_c_scopet scopet; diff --git a/src/ansi-c/builtin_factory.cpp b/src/ansi-c/builtin_factory.cpp index 86f035f960b..529309ce514 100644 --- a/src/ansi-c/builtin_factory.cpp +++ b/src/ansi-c/builtin_factory.cpp @@ -54,6 +54,7 @@ static bool convert( ansi_c_parser.ts_18661_3_Floatn_types = config.ansi_c.ts_18661_3_Floatn_types; ansi_c_parser.float16_type = config.ansi_c.float16_type; ansi_c_parser.bf16_type = config.ansi_c.bf16_type; + ansi_c_parser.fp16_type = config.ansi_c.fp16_type; ansi_c_parser.cpp98=false; // it's not C++ ansi_c_parser.cpp11=false; // it's not C++ ansi_c_parser.mode=config.ansi_c.mode; diff --git a/src/ansi-c/gcc_version.cpp b/src/ansi-c/gcc_version.cpp index f36318f16d9..4b3e35cb34e 100644 --- a/src/ansi-c/gcc_version.cpp +++ b/src/ansi-c/gcc_version.cpp @@ -174,4 +174,11 @@ void configure_gcc(const gcc_versiont &gcc_version) gcc_version.is_at_least(13u)) || (gcc_version.flavor == gcc_versiont::flavort::CLANG && gcc_version.is_at_least(15u)); + + config.ansi_c.fp16_type = + (gcc_version.flavor == gcc_versiont::flavort::GCC && + gcc_version.is_at_least(4u, 5u) && + (config.ansi_c.arch == "arm" || config.ansi_c.arch == "arm64")) || + (gcc_version.flavor == gcc_versiont::flavort::CLANG && + gcc_version.is_at_least(6u)); } diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 7d3c135f6fd..5dc5cb5a0ca 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -546,6 +546,12 @@ enable_or_disable ("enable"|"disable") return make_identifier(); } +"__fp16" { if(PARSER.fp16_type) + { loc(); return TOK_GCC_FLOAT16; } + else + return make_identifier(); + } + "_Float32" { if(PARSER.ts_18661_3_Floatn_types) { loc(); return TOK_GCC_FLOAT32; } else diff --git a/src/cpp/cpp_parser.cpp b/src/cpp/cpp_parser.cpp index 5190dc7d14d..390dffaeeac 100644 --- a/src/cpp/cpp_parser.cpp +++ b/src/cpp/cpp_parser.cpp @@ -42,6 +42,7 @@ bool cpp_parsert::parse() false; // these are still typedefs token_buffer.ansi_c_parser.float16_type = *support_float16; token_buffer.ansi_c_parser.bf16_type = *support_float16; + token_buffer.ansi_c_parser.fp16_type = *support_float16; token_buffer.ansi_c_parser.in = in; token_buffer.ansi_c_parser.mode = mode; token_buffer.ansi_c_parser.set_file(get_file()); diff --git a/src/goto-instrument/contracts/contracts_wrangler.cpp b/src/goto-instrument/contracts/contracts_wrangler.cpp index 36c8bb117a8..e3b3f9f1cd8 100644 --- a/src/goto-instrument/contracts/contracts_wrangler.cpp +++ b/src/goto-instrument/contracts/contracts_wrangler.cpp @@ -147,6 +147,7 @@ void contracts_wranglert::mangle( ansi_c_parser.ts_18661_3_Floatn_types = config.ansi_c.ts_18661_3_Floatn_types; ansi_c_parser.float16_type = config.ansi_c.float16_type; ansi_c_parser.bf16_type = config.ansi_c.bf16_type; + ansi_c_parser.fp16_type = config.ansi_c.fp16_type; ansi_c_parser.cpp98 = false; // it's not C++ ansi_c_parser.cpp11 = false; // it's not C++ ansi_c_parser.mode = config.ansi_c.mode; diff --git a/src/util/config.cpp b/src/util/config.cpp index c0c999c4cc0..5a09cdb6a22 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -837,6 +837,7 @@ bool configt::set(const cmdlinet &cmdline) ansi_c.ts_18661_3_Floatn_types=false; ansi_c.float16_type = false; ansi_c.bf16_type = false; + ansi_c.fp16_type = false; ansi_c.c_standard=ansi_ct::default_c_standard(); ansi_c.endianness=ansi_ct::endiannesst::NO_ENDIANNESS; ansi_c.os=ansi_ct::ost::NO_OS; @@ -1328,8 +1329,8 @@ void configt::set_from_symbol_table(const symbol_table_baset &symbol_table) ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0; ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0; // for_has_scope, single_precision_constant, rounding_mode, - // ts_18661_3_Floatn_types, float16_type, bf16_type are not architectural - // features, and thus not stored in namespace + // ts_18661_3_Floatn_types, float16_type, bf16_type, fp16_type are not + // architectural features, and thus not stored in namespace ansi_c.alignment=unsigned_from_ns(ns, "alignment"); diff --git a/src/util/config.h b/src/util/config.h index f7bc65c6033..54839f9d337 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -153,6 +153,7 @@ class configt bool gcc__float128_type; // __float128, a gcc extension since 4.3/4.5 bool float16_type; // _Float16 (Clang >= 15, GCC >= 12) bool bf16_type; // __bf16 (Clang >= 15, GCC >= 13) + bool fp16_type; // __fp16 (GCC >= 4.5 on ARM, Clang >= 6) bool single_precision_constant; enum class c_standardt { diff --git a/unit/cpp_scanner.cpp b/unit/cpp_scanner.cpp index 76730e739fe..7d60815da32 100644 --- a/unit/cpp_scanner.cpp +++ b/unit/cpp_scanner.cpp @@ -43,6 +43,7 @@ int main(int argc, const char *argv[]) ansi_c_parser.ts_18661_3_Floatn_types = false; ansi_c_parser.float16_type = false; ansi_c_parser.bf16_type = false; + ansi_c_parser.fp16_type = false; ansi_c_parser.in=∈ cpp_parser.in=∈