diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 52d66fe102b..c6a82b5a1fb 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -583,8 +583,8 @@ jobs: run: cd build; ctest . -V -L THOROUGH -j2 # This job takes approximately 39 to 69 minutes - check-macos-11-make-clang: - runs-on: macos-11 + check-macos-13-make-clang: + runs-on: macos-13 steps: - uses: actions/checkout@v4 with: @@ -617,8 +617,8 @@ jobs: - name: Build using Make run: | make -C src minisat2-download cadical-download - make -C src -j3 CXX="ccache clang++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical - make -C jbmc/src -j3 CXX="ccache clang++" + make -C src -j4 CXX="ccache clang++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical + make -C jbmc/src -j4 CXX="ccache clang++" make -C unit "CXX=ccache clang++" make -C jbmc/unit "CXX=ccache clang++" - name: Print ccache stats @@ -630,9 +630,9 @@ jobs: - name: Run JBMC unit tests run: cd jbmc/unit; ./unit_tests - name: Run regression tests - run: make -C regression test-parallel JOBS=3 + run: make -C regression test-parallel JOBS=4 - name: Run JBMC regression tests - run: make -C jbmc/regression test-parallel JOBS=3 + run: make -C jbmc/regression test-parallel JOBS=4 # This job takes approximately 66 to 85 minutes check-macos-12-cmake-clang: diff --git a/.github/workflows/release-packages.yaml b/.github/workflows/release-packages.yaml index d796791b44e..c8382afedf3 100644 --- a/.github/workflows/release-packages.yaml +++ b/.github/workflows/release-packages.yaml @@ -152,7 +152,7 @@ jobs: SLACK_MESSAGE: "${{ job.status == 'success' && 'Ubuntu 20.04 package built and uploaded successfully' || 'Ubuntu 20.04 package build failed' }}" homebrew-pr: - runs-on: macos-11 + runs-on: macos-13 steps: - name: Get release tag name # The GITHUB_REF we get has refs/tags/ in front of the tag name so we diff --git a/jbmc/regression/jbmc-strings/StringIndexOf/test_thorough.desc b/jbmc/regression/jbmc-strings/StringIndexOf/test_thorough.desc index 18e6bafaf45..320c4c69de4 100644 --- a/jbmc/regression/jbmc-strings/StringIndexOf/test_thorough.desc +++ b/jbmc/regression/jbmc-strings/StringIndexOf/test_thorough.desc @@ -1,7 +1,13 @@ -CORE +THOROUGH Test ---function Test.check --unwind 10 --no-unwinding-assertions --max-nondet-string-length 10 --java-assume-inputs-non-null +--function Test.check --unwind 10 --no-unwinding-assertions --max-nondet-string-length 10 --java-assume-inputs-non-null --sat-solver cadical ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- +-- +This test completes in less than 3 seconds with CaDiCaL +-- +This test completes in less than 3 seconds with CaDiCaL, but may flip between +seconds and several minutes with MiniSat even just changing the order of +equations. diff --git a/regression/cbmc/__builtin_bit_cast-01/main.c b/regression/cbmc/__builtin_bit_cast-01/main.c new file mode 100644 index 00000000000..303c3117ae6 --- /dev/null +++ b/regression/cbmc/__builtin_bit_cast-01/main.c @@ -0,0 +1,15 @@ +#include +#include + +int main() +{ +#if defined(__clang__) || defined(_GNUC_) + // GCC actually only supports __builtin_bit_cast in C++ mode, but we do it for + // C as well. + float f = 1.5; + assert((int32_t)f == 1); + int32_t i = __builtin_bit_cast(int32_t, f); + assert(i != 1); + assert(__builtin_bit_cast(float, i) == f); +#endif +} diff --git a/regression/cbmc/__builtin_bit_cast-01/test.desc b/regression/cbmc/__builtin_bit_cast-01/test.desc new file mode 100644 index 00000000000..278f468e130 --- /dev/null +++ b/regression/cbmc/__builtin_bit_cast-01/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index 6e83d9e592f..4a434bb2f69 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -76,6 +76,7 @@ bool ansi_c_languaget::parse( ansi_c_parser.in=&codestr; ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope; ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types; + ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword; 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; @@ -201,6 +202,7 @@ bool ansi_c_languaget::to_expr( ansi_c_parser.in=&i_preprocessed; ansi_c_parser.for_has_scope = config.ansi_c.for_has_scope; ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types; + ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword; 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; diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h index 206e7be8dda..6128b1b56b9 100644 --- a/src/ansi-c/ansi_c_parser.h +++ b/src/ansi-c/ansi_c_parser.h @@ -36,6 +36,7 @@ class ansi_c_parsert:public parsert cpp11(false), for_has_scope(false), ts_18661_3_Floatn_types(false), + __float128_is_keyword(false), float16_type(false), bf16_type(false), fp16_type(false) @@ -68,6 +69,7 @@ class ansi_c_parsert:public parsert // ISO/IEC TS 18661-3:2015 bool ts_18661_3_Floatn_types; + bool __float128_is_keyword; bool float16_type; bool bf16_type; bool fp16_type; diff --git a/src/ansi-c/builtin_factory.cpp b/src/ansi-c/builtin_factory.cpp index 79ad21a9e60..33e44d24521 100644 --- a/src/ansi-c/builtin_factory.cpp +++ b/src/ansi-c/builtin_factory.cpp @@ -52,6 +52,7 @@ static bool convert( ansi_c_parser.in=∈ ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope; ansi_c_parser.ts_18661_3_Floatn_types = config.ansi_c.ts_18661_3_Floatn_types; + ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword; 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; diff --git a/src/ansi-c/c_expr.cpp b/src/ansi-c/c_expr.cpp index a763f0fb550..8ce2a520bb1 100644 --- a/src/ansi-c/c_expr.cpp +++ b/src/ansi-c/c_expr.cpp @@ -83,3 +83,8 @@ exprt enum_is_in_range_exprt::lower(const namespacet &ns) const return simplify_expr(disjunction(disjuncts), ns); } + +byte_extract_exprt bit_cast_exprt::lower() const +{ + return make_byte_extract(op(), from_integer(0, c_index_type()), type()); +} diff --git a/src/ansi-c/c_expr.h b/src/ansi-c/c_expr.h index 13a7ceca4eb..d0bac3fc77b 100644 --- a/src/ansi-c/c_expr.h +++ b/src/ansi-c/c_expr.h @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com /// \file ansi-c/c_expr.h /// API to expression classes that are internal to the C frontend +#include #include /// \brief Shuffle elements of one or two vectors, modelled after Clang's @@ -370,4 +371,51 @@ inline enum_is_in_range_exprt &to_enum_is_in_range_expr(exprt &expr) return ret; } +/// \brief Reinterpret the bits of an expression of type `S` as an expression of +/// type `T` where `S` and `T` have the same size. +class bit_cast_exprt : public unary_exprt +{ +public: + bit_cast_exprt(exprt expr, typet type) + : unary_exprt(ID_bit_cast, std::move(expr), std::move(type)) + { + } + + byte_extract_exprt lower() const; +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_bit_cast; +} + +inline void validate_expr(const bit_cast_exprt &value) +{ + validate_operands(value, 1, "bit_cast must have one operand"); +} + +/// \brief Cast an exprt to a \ref bit_cast_exprt +/// +/// \a expr must be known to be \ref bit_cast_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref bit_cast_exprt +inline const bit_cast_exprt &to_bit_cast_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_bit_cast); + const bit_cast_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; +} + +/// \copydoc to_bit_cast_expr(const exprt &) +inline bit_cast_exprt &to_bit_cast_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_bit_cast); + bit_cast_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; +} + #endif // CPROVER_ANSI_C_C_EXPR_H diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 1ade7b9c8a6..0ce58dbc2bf 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -497,6 +497,24 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr) { // already type checked } + else if(auto bit_cast_expr = expr_try_dynamic_cast(expr)) + { + typecheck_type(expr.type()); + if( + pointer_offset_bits(bit_cast_expr->type(), *this) == + pointer_offset_bits(bit_cast_expr->op().type(), *this)) + { + exprt tmp = bit_cast_expr->lower(); + expr.swap(tmp); + } + else + { + error().source_location = expr.source_location(); + error() << "bit cast from '" << to_string(bit_cast_expr->op().type()) + << "' to '" << to_string(expr.type()) << "' not permitted" << eom; + throw 0; + } + } else { error().source_location = expr.source_location(); @@ -2151,7 +2169,9 @@ void c_typecheck_baset::typecheck_side_effect_function_call( } else if( identifier == CPROVER_PREFIX "saturating_minus" || - identifier == CPROVER_PREFIX "saturating_plus") + identifier == CPROVER_PREFIX "saturating_plus" || + identifier == "__builtin_elementwise_add_sat" || + identifier == "__builtin_elementwise_sub_sat") { exprt result = typecheck_saturating_arithmetic(expr); expr.swap(result); @@ -3824,10 +3844,18 @@ exprt c_typecheck_baset::typecheck_saturating_arithmetic( } exprt result; - if(identifier == CPROVER_PREFIX "saturating_minus") + if( + identifier == CPROVER_PREFIX "saturating_minus" || + identifier == "__builtin_elementwise_sub_sat") + { result = saturating_minus_exprt{expr.arguments()[0], expr.arguments()[1]}; - else if(identifier == CPROVER_PREFIX "saturating_plus") + } + else if( + identifier == CPROVER_PREFIX "saturating_plus" || + identifier == "__builtin_elementwise_add_sat") + { result = saturating_plus_exprt{expr.arguments()[0], expr.arguments()[1]}; + } else UNREACHABLE; diff --git a/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h b/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h index a2a14147908..4c938502530 100644 --- a/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h +++ b/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h @@ -17,6 +17,9 @@ typedef short __gcc_v4hi __attribute__ ((__vector_size__ (8))); typedef short __gcc_v8hi __attribute__ ((__vector_size__ (16))); typedef short __gcc_v16hi __attribute__ ((__vector_size__ (32))); typedef short __gcc_v32hi __attribute__ ((__vector_size__ (64))); +typedef __CPROVER_Float16 __gcc_v8hf __attribute__ ((__vector_size__ (16))); +typedef __CPROVER_Float16 __gcc_v16hf __attribute__ ((__vector_size__ (32))); +typedef __CPROVER_Float16 __gcc_v32hf __attribute__ ((__vector_size__ (64))); typedef float __gcc_v2sf __attribute__ ((__vector_size__ (8))); typedef float __gcc_v4sf __attribute__ ((__vector_size__ (16))); typedef float __gcc_v8sf __attribute__ ((__vector_size__ (32))); @@ -28,7 +31,10 @@ typedef long long __gcc_v1di __attribute__ ((__vector_size__ (8))); typedef long long __gcc_v2di __attribute__ ((__vector_size__ (16))); typedef long long __gcc_v4di __attribute__ ((__vector_size__ (32))); typedef long long __gcc_v8di __attribute__ ((__vector_size__ (64))); +typedef unsigned short __gcc_v32uhi __attribute__ ((__vector_size__ (64))); +typedef unsigned int __gcc_v16usi __attribute__ ((__vector_size__ (64))); typedef unsigned long long __gcc_di; +typedef unsigned long long __gcc_v8udi __attribute__ ((__vector_size__ (64))); enum __gcc_atomic_memmodels { __ATOMIC_RELAXED, __ATOMIC_CONSUME, __ATOMIC_ACQUIRE, __ATOMIC_RELEASE, __ATOMIC_ACQ_REL, __ATOMIC_SEQ_CST diff --git a/src/ansi-c/gcc_version.cpp b/src/ansi-c/gcc_version.cpp index 4b3e35cb34e..8ce7b950c0e 100644 --- a/src/ansi-c/gcc_version.cpp +++ b/src/ansi-c/gcc_version.cpp @@ -162,6 +162,12 @@ void configure_gcc(const gcc_versiont &gcc_version) config.ansi_c.gcc__float128_type = gcc_version.flavor == gcc_versiont::flavort::GCC && gcc_version.is_at_least(4u, gcc_float128_minor_version); + config.ansi_c.__float128_is_keyword = + gcc_version.flavor == gcc_versiont::flavort::CLANG || + (gcc_version.flavor == gcc_versiont::flavort::GCC && + config.ansi_c.arch == "arm64" && + config.ansi_c.os == configt::ansi_ct::ost::OS_MACOS && + config.ansi_c.gcc__float128_type); config.ansi_c.float16_type = (gcc_version.flavor == gcc_versiont::flavort::GCC && diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 45ecacbc1a1..92ce6cae565 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -236,6 +236,7 @@ int yyansi_cerror(const std::string &error); %token TOK_THREAD_LOCAL "_Thread_local" %token TOK_NULLPTR "nullptr" %token TOK_CONSTEXPR "constexpr" +%token TOK_BIT_CAST "__builtin_bit_cast" /*** special scanner reports ***/ @@ -715,6 +716,12 @@ unary_expression: parser_stack($$).id(ID_alignof); parser_stack($$).add(ID_type_arg).swap(parser_stack($3)); } + | TOK_BIT_CAST '(' type_name ',' unary_expression ')' + { $$=$1; + set($$, ID_bit_cast); + mto($$, $5); + parser_stack($$).type().swap(parser_stack($3)); + } ; cast_expression: diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 5dc5cb5a0ca..ac122dd7612 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -540,6 +540,10 @@ enable_or_disable ("enable"|"disable") return make_identifier(); } +{CPROVER_PREFIX}"Float16" { + loc(); return TOK_GCC_FLOAT16; + } + "__bf16" { if(PARSER.bf16_type) { loc(); return TOK_GCC_FLOAT16; } else @@ -584,9 +588,7 @@ enable_or_disable ("enable"|"disable") loc(); return TOK_GCC_FLOAT80; } -"__float128" { // This is a keyword for CLANG, - // but a typedef for GCC - if(PARSER.mode==configt::ansi_ct::flavourt::CLANG) +"__float128" { if(PARSER.__float128_is_keyword) { loc(); return TOK_GCC_FLOAT128; } else return make_identifier(); @@ -1307,6 +1309,13 @@ __decltype { if(PARSER.cpp98 && return make_identifier(); } +"__builtin_bit_cast" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC || + PARSER.mode==configt::ansi_ct::flavourt::CLANG) + { loc(); return TOK_BIT_CAST; } + else + return make_identifier(); + } + {CPROVER_PREFIX}"atomic" { loc(); return TOK_CPROVER_ATOMIC; } {CPROVER_PREFIX}"forall" { loc(); return TOK_FORALL; } {CPROVER_PREFIX}"exists" { loc(); return TOK_EXISTS; } diff --git a/src/cpp/cpp_parser.cpp b/src/cpp/cpp_parser.cpp index 390dffaeeac..4f3f30d58c5 100644 --- a/src/cpp/cpp_parser.cpp +++ b/src/cpp/cpp_parser.cpp @@ -40,6 +40,7 @@ bool cpp_parsert::parse() config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP17; token_buffer.ansi_c_parser.ts_18661_3_Floatn_types = false; // these are still typedefs + token_buffer.ansi_c_parser.__float128_is_keyword = false; 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; diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index ad28a403bde..777f4b2f0bd 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -772,11 +772,12 @@ bool Parser::isTypeSpecifier() || t == TOK_SIGNED || t == TOK_UNSIGNED || t == TOK_FLOAT || t == TOK_DOUBLE || t == TOK_INT8 || t == TOK_INT16 || t == TOK_INT32 || t == TOK_INT64 || t == TOK_GCC_INT128 || t == TOK_PTR32 || - t == TOK_PTR64 || t == TOK_GCC_FLOAT80 || t == TOK_GCC_FLOAT128 || - t == TOK_VOID || t == TOK_BOOL || t == TOK_CPROVER_BOOL || - t == TOK_CLASS || t == TOK_STRUCT || t == TOK_UNION || t == TOK_ENUM || - t == TOK_INTERFACE || t == TOK_TYPENAME || t == TOK_TYPEOF || - t == TOK_DECLTYPE || t == TOK_UNDERLYING_TYPE; + t == TOK_PTR64 || t == TOK_GCC_FLOAT16 || t == TOK_GCC_FLOAT80 || + t == TOK_GCC_FLOAT128 || t == TOK_VOID || t == TOK_BOOL || + t == TOK_CPROVER_BOOL || t == TOK_CLASS || t == TOK_STRUCT || + t == TOK_UNION || t == TOK_ENUM || t == TOK_INTERFACE || + t == TOK_TYPENAME || t == TOK_TYPEOF || t == TOK_DECLTYPE || + t == TOK_UNDERLYING_TYPE; } /* @@ -2510,6 +2511,9 @@ bool Parser::optIntegralTypeOrClassSpec(typet &p) case TOK_INT32: type_id=ID_int32; break; case TOK_INT64: type_id=ID_int64; break; case TOK_GCC_INT128: type_id=ID_gcc_int128; break; + case TOK_GCC_FLOAT16: + type_id = ID_gcc_float16; + break; case TOK_GCC_FLOAT80: type_id=ID_gcc_float80; break; case TOK_GCC_FLOAT128: type_id=ID_gcc_float128; break; case TOK_BOOL: diff --git a/src/goto-instrument/contracts/contracts_wrangler.cpp b/src/goto-instrument/contracts/contracts_wrangler.cpp index e3b3f9f1cd8..e66d6f52421 100644 --- a/src/goto-instrument/contracts/contracts_wrangler.cpp +++ b/src/goto-instrument/contracts/contracts_wrangler.cpp @@ -145,6 +145,7 @@ void contracts_wranglert::mangle( ansi_c_parser.in = &is; ansi_c_parser.for_has_scope = config.ansi_c.for_has_scope; ansi_c_parser.ts_18661_3_Floatn_types = config.ansi_c.ts_18661_3_Floatn_types; + ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword; 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; diff --git a/src/util/config.cpp b/src/util/config.cpp index 5a09cdb6a22..477e028d386 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -835,6 +835,7 @@ bool configt::set(const cmdlinet &cmdline) ansi_c.single_precision_constant=false; ansi_c.for_has_scope=true; // C99 or later ansi_c.ts_18661_3_Floatn_types=false; + ansi_c.__float128_is_keyword = false; ansi_c.float16_type = false; ansi_c.bf16_type = false; ansi_c.fp16_type = false; @@ -985,6 +986,13 @@ bool configt::set(const cmdlinet &cmdline) ansi_c.os=configt::ansi_ct::ost::OS_MACOS; ansi_c.mode = ansi_ct::flavourt::CLANG; ansi_c.preprocessor=ansi_ct::preprocessort::CLANG; + // configure_gcc sets these with additional version-of-clang level of + // detail, but the below are reasonable defaults for modern clang + // installations + ansi_c.__float128_is_keyword = true; + ansi_c.float16_type = true; + ansi_c.bf16_type = true; + ansi_c.fp16_type = true; } else if(os == "linux" || os == "solaris" || os == "netbsd" || os == "hurd") { @@ -999,6 +1007,13 @@ bool configt::set(const cmdlinet &cmdline) ansi_c.os=configt::ansi_ct::ost::OS_LINUX; ansi_c.mode=ansi_ct::flavourt::CLANG; ansi_c.preprocessor=ansi_ct::preprocessort::CLANG; + // configure_gcc sets these with additional version-of-clang level of + // detail, but the below are reasonable defaults for modern clang + // installations + ansi_c.__float128_is_keyword = true; + ansi_c.float16_type = true; + ansi_c.bf16_type = true; + ansi_c.fp16_type = true; } else { @@ -1329,8 +1344,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, fp16_type are not - // architectural features, and thus not stored in namespace + // ts_18661_3_Floatn_types, __float128_is_keyword, 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 54839f9d337..e22e68528c4 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -151,6 +151,7 @@ class configt bool for_has_scope; bool ts_18661_3_Floatn_types; // ISO/IEC TS 18661-3:2015 bool gcc__float128_type; // __float128, a gcc extension since 4.3/4.5 + bool __float128_is_keyword; // __float128 as a keyword (and not typedef) 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) diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index a3df1ff0ae4..f1728411191 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -914,6 +914,7 @@ IREP_ID_ONE(prophecy_rw_ok) IREP_ID_ONE(prophecy_r_ok) IREP_ID_ONE(prophecy_w_ok) IREP_ID_ONE(prophecy_pointer_in_range) +IREP_ID_ONE(bit_cast) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree diff --git a/unit/cpp_scanner.cpp b/unit/cpp_scanner.cpp index 7d60815da32..4000994f015 100644 --- a/unit/cpp_scanner.cpp +++ b/unit/cpp_scanner.cpp @@ -41,6 +41,7 @@ int main(int argc, const char *argv[]) ansi_c_parser.cpp98=true; ansi_c_parser.cpp11=false; ansi_c_parser.ts_18661_3_Floatn_types = false; + ansi_c_parser.__float128_is_keyword = false; ansi_c_parser.float16_type = false; ansi_c_parser.bf16_type = false; ansi_c_parser.fp16_type = false;