Add support for building with GCC 14

.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 @@
     {
       // 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 @@
 #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,