From 560a5886895677237635fa0acafce22f38960e6d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 5 Jul 2024 13:14:45 +0000 Subject: [PATCH] Add support for building with GCC 14 GCC 14 adds new warnings. Those are largely spurious (perhaps with exception of the interpreter code and unit tests), but still require working around. These warnings also affect CaDiCaL builds, which in turn requires us to upgrade to version 2.0.0, where workarounds have been added. Fixes: #7749 --- .github/workflows/pull-request-checks.yaml | 20 ++++++++--------- .../java_bytecode/assignments_from_json.cpp | 5 +++-- jbmc/src/java_bytecode/java_utils.h | 6 ++++- jbmc/src/java_bytecode/lambda_synthesis.cpp | 6 ++++- .../require_goto_statements.cpp | 5 ++--- .../require_goto_statements.h | 4 ++-- jbmc/unit/java-testing-utils/require_type.h | 3 +++ ...adical-1.7.2-patch => cadical-2.0.0-patch} | 0 scripts/cadical_CMakeLists.txt | 2 +- src/Makefile | 4 ++-- .../gcc_builtin_headers_types.h | 4 ++++ .../contracts/dynamic-frames/dfcc_utils.h | 12 ++++++++-- src/goto-programs/interpreter.cpp | 4 ++-- src/goto-programs/mm_io.cpp | 17 +++++++------- src/goto-symex/goto_symex.cpp | 22 ++++++++++--------- src/goto-symex/shadow_memory.cpp | 18 ++++++++------- src/goto-symex/symex_dereference.cpp | 18 +++++++-------- src/solvers/CMakeLists.txt | 12 +++++----- src/solvers/Makefile | 2 +- src/util/fresh_symbol.h | 12 ++++++++-- src/util/irep.h | 6 ++++- unit/testing-utils/require_symbol.h | 6 ++++- unit/util/graph.cpp | 10 ++++++++- 23 files changed, 124 insertions(+), 74 deletions(-) rename scripts/{cadical-1.7.2-patch => cadical-2.0.0-patch} (100%) diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index eb79155a337..023ccfc81c7 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -399,7 +399,7 @@ jobs: run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}} # This job takes approximately 14 to 46 minutes - check-ubuntu-24_04-cmake-gcc-13: + check-ubuntu-24_04-cmake-gcc-14: runs-on: ubuntu-24.04 steps: - uses: actions/checkout@v4 @@ -412,13 +412,13 @@ jobs: DEBIAN_FRONTEND: noninteractive run: | sudo apt-get update - sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc-13 gdb g++-13 maven flex bison libxml2-utils dpkg-dev ccache doxygen z3 + sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc-14 gdb g++-14 maven flex bison libxml2-utils dpkg-dev ccache doxygen z3 # Update symlinks so that any use of gcc (including our regression - # tests) will use GCC 13. - sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-13 110 \ - --slave /usr/bin/g++ g++ /usr/bin/g++-13 \ - --slave /usr/bin/gcov gcov /usr/bin/gcov-13 - sudo ln -sf cpp-13 /usr/bin/cpp + # tests) will use GCC 14. + sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-14 110 \ + --slave /usr/bin/g++ g++ /usr/bin/g++-14 \ + --slave /usr/bin/gcov gcov /usr/bin/gcov-14 + sudo ln -sf cpp-14 /usr/bin/cpp - name: Confirm z3 solver is available and log the version installed run: z3 --version - name: Download cvc-5 from the releases page and make sure it can be deployed @@ -432,10 +432,10 @@ jobs: with: save-always: true path: .ccache - key: ${{ runner.os }}-24.04-Release-gcc-13-${{ github.ref }}-${{ github.sha }}-PR + key: ${{ runner.os }}-24.04-Release-gcc-14-${{ github.ref }}-${{ github.sha }}-PR restore-keys: | - ${{ runner.os }}-24.04-Release-gcc-13-${{ github.ref }} - ${{ runner.os }}-24.04-Release-gcc-13 + ${{ runner.os }}-24.04-Release-gcc-14-${{ github.ref }} + ${{ runner.os }}-24.04-Release-gcc-14 - name: ccache environment run: | echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp index 117aeb49c17..d4e3f6e7308 100644 --- a/jbmc/src/java_bytecode/assignments_from_json.cpp +++ b/jbmc/src/java_bytecode/assignments_from_json.cpp @@ -641,8 +641,9 @@ static code_with_references_listt assign_enum_from_json( dereference_exprt values_struct{ info.symbol_table.lookup_ref(values_name).symbol_expr()}; - const auto &values_struct_type = namespacet{info.symbol_table}.follow_tag( - to_struct_tag_type(values_struct.type())); + const namespacet ns{info.symbol_table}; + const auto &values_struct_type = + ns.follow_tag(to_struct_tag_type(values_struct.type())); PRECONDITION(is_valid_java_array(values_struct_type)); const member_exprt values_data = member_exprt{ values_struct, "data", values_struct_type.components()[2].type()}; diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index c07e2a716aa..4deb6183cde 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/jbmc/src/java_bytecode/java_utils.h @@ -164,7 +164,11 @@ bool is_non_null_library_global(const irep_idt &); extern const std::unordered_set cprover_methods_to_ignore; -symbolt &fresh_java_symbol( +#if defined(__GNUC__) && __GNUC__ >= 14 +[[gnu::no_dangling]] +#endif +symbolt & +fresh_java_symbol( const typet &type, const std::string &basename_prefix, const source_locationt &source_location, diff --git a/jbmc/src/java_bytecode/lambda_synthesis.cpp b/jbmc/src/java_bytecode/lambda_synthesis.cpp index 559acb80b04..8fa28b18159 100644 --- a/jbmc/src/java_bytecode/lambda_synthesis.cpp +++ b/jbmc/src/java_bytecode/lambda_synthesis.cpp @@ -444,7 +444,11 @@ void create_invokedynamic_synthetic_classes( } } -static const symbolt &get_or_create_method_symbol( +#if defined(__GNUC__) && __GNUC__ >= 14 +[[gnu::no_dangling]] +#endif +static const symbolt & +get_or_create_method_symbol( const irep_idt &identifier, const irep_idt &base_name, const irep_idt &pretty_name, diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp index 81248f7b8e8..f95bbcff992 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.cpp +++ b/jbmc/unit/java-testing-utils/require_goto_statements.cpp @@ -381,7 +381,7 @@ get_ultimate_source_symbol( /// \return The identifier of the ultimate source symbol assigned to the field, /// which will be used for future calls to /// `require_struct_component_assignment`. -const irep_idt &require_goto_statements::require_struct_component_assignment( +irep_idt require_goto_statements::require_struct_component_assignment( const irep_idt &structure_name, const std::optional &superclass_name, const irep_idt &component_name, @@ -514,8 +514,7 @@ require_goto_statements::require_struct_array_component_assignment( /// \param argument_name: Name of the input argument of method under test /// \param entry_point_statements: The statements to look through /// \return The identifier of the variable assigned to the input argument -const irep_idt & -require_goto_statements::require_entry_point_argument_assignment( +irep_idt require_goto_statements::require_entry_point_argument_assignment( const irep_idt &argument_name, const std::vector &entry_point_statements) { diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.h b/jbmc/unit/java-testing-utils/require_goto_statements.h index ebd78d9d7e4..991286e7c2a 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.h +++ b/jbmc/unit/java-testing-utils/require_goto_statements.h @@ -72,7 +72,7 @@ const code_declt &require_declaration_of_name( const irep_idt &variable_name, const std::vector &entry_point_instructions); -const irep_idt &require_struct_component_assignment( +irep_idt require_struct_component_assignment( const irep_idt &structure_name, const std::optional &superclass_name, const irep_idt &component_name, @@ -89,7 +89,7 @@ const irep_idt &require_struct_array_component_assignment( const std::vector &entry_point_instructions, const symbol_table_baset &symbol_table); -const irep_idt &require_entry_point_argument_assignment( +irep_idt require_entry_point_argument_assignment( const irep_idt &argument_name, const std::vector &entry_point_statements); diff --git a/jbmc/unit/java-testing-utils/require_type.h b/jbmc/unit/java-testing-utils/require_type.h index 513593fb7cc..84f3b51015e 100644 --- a/jbmc/unit/java-testing-utils/require_type.h +++ b/jbmc/unit/java-testing-utils/require_type.h @@ -24,6 +24,9 @@ namespace require_type pointer_typet require_pointer(const typet &type, const std::optional &subtype); +#if defined(__GNUC__) && __GNUC__ >= 14 +[[gnu::no_dangling]] +#endif const struct_tag_typet & require_struct_tag(const typet &type, const irep_idt &identifier = ""); diff --git a/scripts/cadical-1.7.2-patch b/scripts/cadical-2.0.0-patch similarity index 100% rename from scripts/cadical-1.7.2-patch rename to scripts/cadical-2.0.0-patch diff --git a/scripts/cadical_CMakeLists.txt b/scripts/cadical_CMakeLists.txt index 9dcb6d27230..c3c0343920e 100644 --- a/scripts/cadical_CMakeLists.txt +++ b/scripts/cadical_CMakeLists.txt @@ -9,7 +9,7 @@ add_library(cadical ${sources}) # Pass -DNBUILD to disable including the version information, which is not # needed since cbmc doesn't run the cadical binary -target_compile_options(cadical PUBLIC -DNBUILD) +target_compile_options(cadical PUBLIC -DNBUILD -DNFLEXIBLE) set_target_properties( cadical diff --git a/src/Makefile b/src/Makefile index e9181a2e039..4b3c4eb5cc7 100644 --- a/src/Makefile +++ b/src/Makefile @@ -186,14 +186,14 @@ glucose-download: @(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch) @$(RM) $(glucose_rev).tar.gz -cadical_release = rel-1.7.2 +cadical_release = rel-2.0.0 cadical-download: @echo "Downloading CaDiCaL $(cadical_release)" @$(DOWNLOADER) https://github.com/arminbiere/cadical/archive/$(cadical_release).tar.gz @$(TAR) xfz $(cadical_release).tar.gz @rm -Rf ../cadical @mv cadical-$(cadical_release) ../cadical - @(cd ../cadical; patch -p1 < ../scripts/cadical-1.7.2-patch) + @(cd ../cadical; patch -p1 < ../scripts/cadical-2.0.0-patch) @(cd ../cadical && ./configure CXX="$(CXX)") # Need to rename VERSION so that it isn't picked up by `#include` on # macOS which is case insensitive 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 4c938502530..8920a952f1d 100644 --- a/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h +++ b/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h @@ -32,8 +32,12 @@ 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_v4usi __attribute__ ((__vector_size__ (16))); +typedef unsigned int __gcc_v8usi __attribute__ ((__vector_size__ (32))); typedef unsigned int __gcc_v16usi __attribute__ ((__vector_size__ (64))); typedef unsigned long long __gcc_di; +typedef unsigned long long __gcc_v2udi __attribute__ ((__vector_size__ (16))); +typedef unsigned long long __gcc_v4udi __attribute__ ((__vector_size__ (32))); typedef unsigned long long __gcc_v8udi __attribute__ ((__vector_size__ (64))); enum __gcc_atomic_memmodels { diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h index 7923947bd4f..f7f57896123 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h @@ -72,7 +72,11 @@ struct dfcc_utilst const bool no_nondet_initialization = true); /// Creates a new parameter symbol for the given function_id - static const symbolt &create_new_parameter_symbol( +#if defined(__GNUC__) && __GNUC__ >= 14 + [[gnu::no_dangling]] +#endif + static const symbolt & + create_new_parameter_symbol( symbol_table_baset &, const irep_idt &function_id, const std::string &base_name, @@ -100,7 +104,11 @@ struct dfcc_utilst /// The cloned function symbol has `new_function_id` as name /// The cloned parameters symbols have `new_function_id::name` as name /// Returns the new function symbol - static const symbolt &clone_and_rename_function( +#if defined(__GNUC__) && __GNUC__ >= 14 + [[gnu::no_dangling]] +#endif + static const symbolt & + clone_and_rename_function( goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &new_function_id, diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 29d0f766f56..3104f1d9de8 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -607,7 +607,7 @@ exprt interpretert::get_value( { // We want the symbol pointed to mp_integer address = rhs[numeric_cast_v(offset)]; - const symbol_exprt &symbol_expr = address_to_symbol(address); + const symbol_exprt symbol_expr = address_to_symbol(address); mp_integer offset_from_address = address_to_offset(address); if(offset_from_address == 0) @@ -751,7 +751,7 @@ void interpretert::execute_function_call() #if 0 const memory_cellt &cell=memory[address]; #endif - const irep_idt &identifier = address_to_symbol(address).get_identifier(); + const irep_idt identifier = address_to_symbol(address).get_identifier(); trace_step.called_function = identifier; const goto_functionst::function_mapt::const_iterator f_it= diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index ad6d0753e01..0db64f9e5aa 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -54,15 +54,14 @@ mm_iot::mm_iot(symbol_table_baset &symbol_table) { mm_io_r = mm_io_r_symbol->symbol_expr(); - const auto &value_symbol = get_fresh_aux_symbol( - to_code_type(mm_io_r.type()).return_type(), - id2string(id_r) + "$value", - id2string(id_r) + "$value", - mm_io_r_symbol->location, - mm_io_r_symbol->mode, - symbol_table); - - mm_io_r_value = value_symbol.symbol_expr(); + mm_io_r_value = get_fresh_aux_symbol( + to_code_type(mm_io_r.type()).return_type(), + id2string(id_r) + "$value", + id2string(id_r) + "$value", + mm_io_r_symbol->location, + mm_io_r_symbol->mode, + symbol_table) + .symbol_expr(); } if(const auto mm_io_w_symbol = symbol_table.lookup(id_w)) diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index f2c88ae4b1b..375a681b83c 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -347,16 +347,18 @@ void goto_symext::associate_array_to_pointer( const function_application_exprt array_to_pointer_app{ function_symbol.symbol_expr(), {new_char_array, string_data}}; - const symbolt &return_symbol = get_fresh_aux_symbol( - to_mathematical_function_type(function_symbol.type).codomain(), - "", - "return_value", - source_locationt(), - function_symbol.mode, - ns, - state.symbol_table); - - const ssa_exprt ssa_expr(return_symbol.symbol_expr()); + symbol_exprt return_symbol_expr = + get_fresh_aux_symbol( + to_mathematical_function_type(function_symbol.type).codomain(), + "", + "return_value", + source_locationt(), + function_symbol.mode, + ns, + state.symbol_table) + .symbol_expr(); + + const ssa_exprt ssa_expr(return_symbol_expr); symex_assign.assign_symbol( ssa_expr, expr_skeletont{}, array_to_pointer_app, {}); diff --git a/src/goto-symex/shadow_memory.cpp b/src/goto-symex/shadow_memory.cpp index b5f5b0358d4..fe7b2005d53 100644 --- a/src/goto-symex/shadow_memory.cpp +++ b/src/goto-symex/shadow_memory.cpp @@ -71,17 +71,19 @@ const symbol_exprt &shadow_memoryt::add_field( const typet &field_type) { const auto &function_symbol = ns.lookup(state.source.function_id); - const symbolt &new_symbol = get_fresh_aux_symbol( - field_type, - id2string(state.source.function_id), - SHADOW_MEMORY_PREFIX + from_expr(expr) + "__" + id2string(field_name), - state.source.pc->source_location(), - function_symbol.mode, - state.symbol_table); + symbol_exprt new_symbol_expr = + get_fresh_aux_symbol( + field_type, + id2string(state.source.function_id), + SHADOW_MEMORY_PREFIX + from_expr(expr) + "__" + id2string(field_name), + state.source.pc->source_location(), + function_symbol.mode, + state.symbol_table) + .symbol_expr(); auto &addresses = state.shadow_memory.address_fields[field_name]; addresses.push_back( - shadow_memory_statet::shadowed_addresst{expr, new_symbol.symbol_expr()}); + shadow_memory_statet::shadowed_addresst{expr, new_symbol_expr}); return addresses.back().shadow; } diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index f4beccfb669..25a61e2f74e 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -215,14 +215,15 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state) return *cached; } - auto const &cache_symbol = get_fresh_aux_symbol( - cache_key.type(), - "symex", - "dereference_cache", - dereference_result.source_location(), - language_mode, - ns, - state.symbol_table); + auto cache_symbol_expr = get_fresh_aux_symbol( + cache_key.type(), + "symex", + "dereference_cache", + dereference_result.source_location(), + language_mode, + ns, + state.symbol_table) + .symbol_expr(); // we need to lift possible lets // (come from the value set to avoid repeating complex pointer comparisons) @@ -237,7 +238,6 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state) symex_config, target}; - auto cache_symbol_expr = cache_symbol.symbol_expr(); assign.assign_symbol( to_ssa_expr(state.rename(cache_symbol_expr, ns).get()), expr_skeletont{}, diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index f17e389a7e8..003a0d957b1 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -121,11 +121,11 @@ foreach(SOLVER ${sat_impl}) message(STATUS "Building solvers with cadical") download_project(PROJ cadical - URL https://github.com/arminbiere/cadical/archive/rel-1.7.2.tar.gz - PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.7.2-patch + URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-2.0.0-patch COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/cadical_CMakeLists.txt CMakeLists.txt COMMAND ./configure - URL_MD5 be646831a017f81b300664e58deba1b5 + URL_MD5 9fc2a66196b86adceb822a583318cc35 ) add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR}) @@ -144,10 +144,10 @@ foreach(SOLVER ${sat_impl}) message(STATUS "Building with IPASIR solver linking against: CaDiCaL") download_project(PROJ cadical - URL https://github.com/arminbiere/cadical/archive/rel-1.7.2.tar.gz - PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.7.2-patch + URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-2.0.0-patch COMMAND ./configure - URL_MD5 be646831a017f81b300664e58deba1b5 + URL_MD5 9fc2a66196b86adceb822a583318cc35 ) message(STATUS "Building CaDiCaL") diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 6c46d6e048f..ad1b777b6a8 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -281,7 +281,7 @@ solvers$(LIBEXT): $(OBJ) $(SOLVER_LIB) $(LINKLIB) ../../cadical/build/libcadical$(LIBEXT): - $(MAKE) $(MAKEARGS) -C $(CADICAL)/build libcadical.a CXX="$(CXX)" CXXFLAGS="$(CP_CXXFLAGS)" + $(MAKE) $(MAKEARGS) -C $(CADICAL)/build libcadical.a CXX="$(CXX)" CXXFLAGS="$(CP_CXXFLAGS) -DNFLEXIBLE" -include smt2/smt2_solver$(DEPEXT) diff --git a/src/util/fresh_symbol.h b/src/util/fresh_symbol.h index 0bab21812be..72d2ca22ac7 100644 --- a/src/util/fresh_symbol.h +++ b/src/util/fresh_symbol.h @@ -22,7 +22,11 @@ class symbolt; class symbol_table_baset; class typet; -symbolt &get_fresh_aux_symbol( +#if defined(__GNUC__) && __GNUC__ >= 14 +[[gnu::no_dangling]] +#endif +symbolt & +get_fresh_aux_symbol( const typet &type, const std::string &name_prefix, const std::string &basename_prefix, @@ -30,7 +34,11 @@ symbolt &get_fresh_aux_symbol( const irep_idt &symbol_mode, symbol_table_baset &symbol_table); -symbolt &get_fresh_aux_symbol( +#if defined(__GNUC__) && __GNUC__ >= 14 +[[gnu::no_dangling]] +#endif +symbolt & +get_fresh_aux_symbol( const typet &type, const std::string &name_prefix, const std::string &basename_prefix, diff --git a/src/util/irep.h b/src/util/irep.h index 97fea5e9c4a..28f87062c48 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -37,7 +37,11 @@ typedef dstringt irep_idt; // NOLINTNEXTLINE(readability/identifiers) typedef dstring_hash irep_id_hash; -inline const std::string &id2string(const irep_idt &d) +#if defined(__GNUC__) && __GNUC__ >= 14 +[[gnu::no_dangling]] +#endif +inline const std::string & +id2string(const irep_idt &d) { return as_string(d); } diff --git a/unit/testing-utils/require_symbol.h b/unit/testing-utils/require_symbol.h index 8bd9d65a3d5..846b17d10df 100644 --- a/unit/testing-utils/require_symbol.h +++ b/unit/testing-utils/require_symbol.h @@ -20,7 +20,11 @@ class symbolt; // NOLINTNEXTLINE(readability/namespace) namespace require_symbol { -const symbolt &require_symbol_exists( +#if defined(__GNUC__) && __GNUC__ >= 14 +[[gnu::no_dangling]] +#endif +const symbolt & +require_symbol_exists( const symbol_tablet &symbol_table, const irep_idt &symbol_identifier); } diff --git a/unit/util/graph.cpp b/unit/util/graph.cpp index 30afb8f2441..ef64dbf4207 100644 --- a/unit/util/graph.cpp +++ b/unit/util/graph.cpp @@ -70,7 +70,15 @@ static bool contains_hole( continue; } + // Work around spurious GCC 14 warning about __builtin_memmove accessing + // elements out-of-bounds +#pragma GCC diagnostic push +#ifndef __clang__ +# pragma GCC diagnostic ignored "-Warray-bounds" +# pragma GCC diagnostic ignored "-Wstringop-overflow" +#endif std::vector::node_indext> extended_cycle = cycle_so_far; +#pragma GCC diagnostic pop extended_cycle.push_back(successor.first); if(contains_hole(g, extended_cycle)) return true; @@ -88,7 +96,7 @@ static bool contains_hole(const grapht &g) for(typename grapht::node_indext i = 0; i < g.size(); ++i) { - std::vector::node_indext> start_node {i}; + std::vector::node_indext> start_node(1, i); if(contains_hole(g, start_node)) return true; }