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

@@ -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

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()};

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<std::string> 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,

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,

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<irep_idt> &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<codet> &entry_point_statements)
 {

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<codet> &entry_point_instructions);
 
-const irep_idt &require_struct_component_assignment(
+irep_idt require_struct_component_assignment(
   const irep_idt &structure_name,
   const std::optional<irep_idt> &superclass_name,
   const irep_idt &component_name,
@@ -89,7 +89,7 @@ const irep_idt &require_struct_array_component_assignment(
   const std::vector<codet> &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<codet> &entry_point_statements);
 

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<typet> &subtype);
 
+#if defined(__GNUC__) && __GNUC__ >= 14
+[[gnu::no_dangling]]
+#endif
 const struct_tag_typet &
 require_struct_tag(const typet &type, const irep_idt &identifier = "");
 

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

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<version>` on
 	# macOS which is case insensitive

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 {

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,

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<std::size_t>(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=

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))

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, {});

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;
 }

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<L1>(cache_symbol_expr, ns).get()),
     expr_skeletont{},

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")

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)
 

src/util/fresh_symbol.h

@@ -22,15 +22,23 @@ 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,
   const source_locationt &source_location,
   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,