From d095367f33d582107a3e344b9008ffabc30cadf9 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Fri, 8 Dec 2023 14:17:47 -0500
Subject: [PATCH 1/5] Update Rust toolchain to `nightly-2023-12-08` (#2926)

Updates the Rust toolchain to `nightly-2023-12-08`. The relevant changes
are:
 * https://github.com/rust-lang/rust/pull/118324
 * https://github.com/rust-lang/rust/pull/118684

---------

Co-authored-by: Celina G. Val <celinval@amazon.com>
---
 .../src/codegen_cprover_gotoc/codegen/operand.rs         | 6 ++++--
 kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs   | 9 ++++-----
 kani-compiler/src/kani_middle/reachability.rs            | 6 +-----
 rust-toolchain.toml                                      | 2 +-
 4 files changed, 10 insertions(+), 13 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index d297d9d90a52..59a18348d582 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -421,7 +421,8 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             (Scalar::Ptr(ptr, _size), _) => {
                 let res_t = self.codegen_ty(ty);
-                let (alloc_id, offset) = ptr.into_parts();
+                let (prov, offset) = ptr.into_parts();
+                let alloc_id = prov.alloc_id();
                 self.codegen_alloc_pointer(res_t, alloc_id, offset, span)
             }
             _ => unimplemented!(),
@@ -646,7 +647,8 @@ impl<'tcx> GotocCtx<'tcx> {
             Size::from_bytes(self.symbol_table.machine_model().pointer_width_in_bytes());
 
         let mut next_offset = Size::ZERO;
-        for &(offset, alloc_id) in alloc.provenance().ptrs().iter() {
+        for &(offset, prov) in alloc.provenance().ptrs().iter() {
+            let alloc_id = prov.alloc_id();
             if offset > next_offset {
                 let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(
                     next_offset.bytes_usize()..offset.bytes_usize(),
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index aec9d8143818..ec5756c4d09b 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -332,11 +332,11 @@ impl<'tcx> GotocCtx<'tcx> {
         ty: Ty<'tcx>,
         args: ty::GenericArgsRef<'tcx>,
     ) -> ty::PolyFnSig<'tcx> {
-        let sig = args.as_coroutine().poly_sig();
+        let sig = args.as_coroutine().sig();
 
-        let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(
-            sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))),
-        );
+        let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(iter::once(
+            ty::BoundVariableKind::Region(ty::BrEnv),
+        ));
         let br = ty::BoundRegion {
             var: ty::BoundVar::from_usize(bound_vars.len() - 1),
             kind: ty::BoundRegionKind::BrEnv,
@@ -349,7 +349,6 @@ impl<'tcx> GotocCtx<'tcx> {
         let pin_args = self.tcx.mk_args(&[env_ty.into()]);
         let env_ty = Ty::new_adt(self.tcx, pin_adt_ref, pin_args);
 
-        let sig = sig.skip_binder();
         // The `FnSig` and the `ret_ty` here is for a coroutines main
         // `coroutine::resume(...) -> CoroutineState` function in case we
         // have an ordinary coroutine, or the `Future::poll(...) -> Poll`
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index a8e7d9fe3f83..216feb66fb87 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -153,11 +153,7 @@ impl<'tcx> MonoItemsCollector<'tcx> {
     /// instruction looking for the items that should be included in the compilation.
     fn reachable_items(&mut self) {
         while let Some(to_visit) = self.queue.pop() {
-            // TODO: This should only check is_foreign_item() or even `has_body()`.
-            // We need https://github.com/rust-lang/rust/pull/118681 to land first.
-            if !self.collected.contains(&to_visit)
-                && !self.tcx.is_foreign_item(rustc_internal::internal(to_visit.clone()).def_id())
-            {
+            if !self.collected.contains(&to_visit) {
                 self.collected.insert(to_visit.clone());
                 let next_items = match &to_visit {
                     MonoItem::Fn(instance) => self.visit_fn(*instance),
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 2bdb5cdf793a..6c7de32c5e63 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-12-07"
+channel = "nightly-2023-12-08"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

From abd3690dce0445ab801b9c5c2bd249b2fb16a526 Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Fri, 8 Dec 2023 23:03:49 +0100
Subject: [PATCH 2/5] Bump docker/login-action from 2 to 3 (#2916)

Bumps [docker/login-action](https://github.com/docker/login-action) from
2 to 3.
---
 .github/workflows/release.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 5a37f5e5c03e..cdc69479d961 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -271,7 +271,7 @@ jobs:
           cargo package -p kani-verifier
 
       - name: 'Login to GitHub Container Registry'
-        uses: docker/login-action@v2
+        uses: docker/login-action@v3
         with:
           registry: ghcr.io
           username: ${{ github.repository_owner }}

From b7ece82280fbfc5025fd6fe95f092728172c58a7 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 8 Dec 2023 23:30:27 -0800
Subject: [PATCH 3/5] Clean up some code before migrating rvalue (#2928)

Clean up old unreachable check due to missing component which has been a
long time by the MirLinker. Also remove an old TODO code to add the def
name to virtual calls. This has regressed before, so the risk of
regressing doesn't seem worth for debug purpose.
---
 .../codegen_cprover_gotoc/codegen/rvalue.rs   | 36 ++++---------------
 .../codegen/statement.rs                      | 15 ++------
 .../src/codegen_cprover_gotoc/codegen/typ.rs  |  2 +-
 .../codegen_cprover_gotoc/context/goto_ctx.rs |  5 ---
 .../src/codegen_cprover_gotoc/utils/names.rs  |  9 ++---
 5 files changed, 12 insertions(+), 55 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index c781f272fb2d..8ded0b7f421a 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -11,7 +11,7 @@ use crate::kani_middle::coercion::{
 };
 use crate::unwrap_or_return_codegen_unimplemented;
 use cbmc::goto_program::{
-    arithmetic_overflow_result_type, BinaryOperator, Expr, Location, Stmt, Symbol, Type,
+    arithmetic_overflow_result_type, BinaryOperator, Expr, Location, Stmt, Type,
     ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
 };
 use cbmc::MachineModel;
@@ -1169,7 +1169,7 @@ impl<'tcx> GotocCtx<'tcx> {
         idx: usize,
     ) -> Expr {
         debug!(?instance, typ=?t, %idx, "codegen_vtable_method_field");
-        let vtable_field_name = self.vtable_field_name(instance.def_id(), idx);
+        let vtable_field_name = self.vtable_field_name(idx);
         let vtable_type = Type::struct_tag(self.vtable_name(t));
         let field_type =
             vtable_type.lookup_field_type(vtable_field_name, &self.symbol_table).unwrap();
@@ -1232,34 +1232,10 @@ impl<'tcx> GotocCtx<'tcx> {
                 .address_of()
                 .cast_to(trait_fn_ty)
         } else {
-            // We skip an entire submodule of the standard library, so drop is missing
-            // for it. Build and insert a function that just calls an unimplemented block
-            // to maintain soundness.
-            let drop_sym_name = format!("drop_unimplemented_{}", self.symbol_name(drop_instance));
-            let pretty_name =
-                format!("drop_unimplemented<{}>", self.readable_instance_name(drop_instance));
-            let drop_sym = self.ensure(&drop_sym_name, |ctx, name| {
-                // Function body
-                let unimplemented = ctx.codegen_unimplemented_stmt(
-                    format!("drop_in_place for {drop_instance}").as_str(),
-                    Location::none(),
-                    "https://github.com/model-checking/kani/issues/281",
-                );
-
-                // Declare symbol for the single, self parameter
-                let param_typ = ctx.codegen_ty(trait_ty).to_pointer();
-                let param_sym = ctx.gen_function_parameter(0, &drop_sym_name, param_typ);
-
-                // Build and insert the function itself
-                Symbol::function(
-                    name,
-                    Type::code(vec![param_sym.to_function_parameter()], Type::empty()),
-                    Some(Stmt::block(vec![unimplemented], Location::none())),
-                    pretty_name,
-                    Location::none(),
-                )
-            });
-            drop_sym.to_expr().address_of().cast_to(trait_fn_ty)
+            unreachable!(
+                "Missing drop implementation for {}",
+                self.readable_instance_name(drop_instance)
+            );
         }
     }
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index a4597885716a..d673c7d37c83 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -6,7 +6,6 @@ use super::PropertyClass;
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
-use rustc_hir::def_id::DefId;
 use rustc_middle::mir;
 use rustc_middle::mir::{
     AssertKind, BasicBlock, NonDivergingIntrinsic, Operand, Place, Statement, StatementKind,
@@ -541,16 +540,9 @@ impl<'tcx> GotocCtx<'tcx> {
                         return Stmt::goto(self.current_fn().find_label(&target.unwrap()), loc);
                     }
                     // Handle a virtual function call via a vtable lookup
-                    InstanceDef::Virtual(def_id, idx) => {
+                    InstanceDef::Virtual(_, idx) => {
                         let self_ty = self.operand_ty(&args[0]);
-                        self.codegen_virtual_funcall(
-                            self_ty,
-                            def_id,
-                            idx,
-                            destination,
-                            &mut fargs,
-                            loc,
-                        )
+                        self.codegen_virtual_funcall(self_ty, idx, destination, &mut fargs, loc)
                     }
                     // Normal, non-virtual function calls
                     InstanceDef::Item(..)
@@ -623,13 +615,12 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_virtual_funcall(
         &mut self,
         self_ty: Ty<'tcx>,
-        def_id: DefId,
         idx: usize,
         place: &Place<'tcx>,
         fargs: &mut [Expr],
         loc: Location,
     ) -> Vec<Stmt> {
-        let vtable_field_name = self.vtable_field_name(def_id, idx);
+        let vtable_field_name = self.vtable_field_name(idx);
         trace!(?self_ty, ?place, ?vtable_field_name, "codegen_virtual_funcall");
         debug!(?fargs, "codegen_virtual_funcall");
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index ec5756c4d09b..3a9d54a384af 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -481,7 +481,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let fn_ptr = fn_ty.to_pointer();
 
         // vtable field name, i.e., 3_vol (idx_method)
-        let vtable_field_name = self.vtable_field_name(instance.def_id(), idx);
+        let vtable_field_name = self.vtable_field_name(idx);
 
         DatatypeComponent::field(vtable_field_name, fn_ptr)
     }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index 01fb198d16fa..6619a6949681 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -138,11 +138,6 @@ impl<'tcx> GotocCtx<'tcx> {
         self.gen_stack_variable(c, fname, "var", t, Location::none(), false)
     }
 
-    // Generate a Symbol Expression representing a function parameter from the MIR
-    pub fn gen_function_parameter(&mut self, c: u64, fname: &str, t: Type) -> Symbol {
-        self.gen_stack_variable(c, fname, "var", t, Location::none(), true)
-    }
-
     /// Given a counter `c` a function name `fname, and a prefix `prefix`, generates a new function local variable
     /// It is an error to reuse an existing `c`, `fname` `prefix` tuple.
     fn gen_stack_variable(
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
index da684b601668..2782f2cee47c 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
@@ -5,7 +5,6 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::InternedString;
-use rustc_hir::def_id::DefId;
 use rustc_hir::def_id::LOCAL_CRATE;
 use rustc_middle::mir::mono::CodegenUnitNameBuilder;
 use rustc_middle::mir::Local;
@@ -83,12 +82,8 @@ impl<'tcx> GotocCtx<'tcx> {
     /// The name for the struct field on a vtable for a given function. Because generic
     /// functions can share the same name, we need to use the index of the entry in the
     /// vtable. This is the same index that will be passed in virtual function calls as
-    /// InstanceDef::Virtual(def_id, idx). We could use solely the index as a key into
-    /// the vtable struct, but we add the method name for debugging readability.
-    ///     Example: 3_vol
-    pub fn vtable_field_name(&self, _def_id: DefId, idx: usize) -> InternedString {
-        // format!("{}_{}", idx, with_no_trimmed_paths!(|| self.tcx.item_name(def_id)))
-        // TODO: use def_id https://github.com/model-checking/kani/issues/364
+    /// InstanceDef::Virtual(def_id, idx).
+    pub fn vtable_field_name(&self, idx: usize) -> InternedString {
         idx.to_string().into()
     }
 

From 9e2b33578cd384c723c6dd0dad40256981b24adf Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Sat, 9 Dec 2023 14:04:12 +0100
Subject: [PATCH 4/5] Bump actions/checkout from 3 to 4 (#2918)

Bumps [actions/checkout](https://github.com/actions/checkout) from 3 to
4.
---
 .github/workflows/audit.yml             |  2 +-
 .github/workflows/bench.yml             |  4 ++--
 .github/workflows/cbmc-latest.yml       |  8 ++++----
 .github/workflows/cbmc-update.yml       |  2 +-
 .github/workflows/extra_jobs.yml        |  2 +-
 .github/workflows/format-check.yml      |  4 ++--
 .github/workflows/kani-m1.yml           |  2 +-
 .github/workflows/kani.yml              | 10 +++++-----
 .github/workflows/release.yml           | 10 +++++-----
 .github/workflows/slow-tests.yml        |  2 +-
 .github/workflows/toolchain-upgrade.yml |  2 +-
 11 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/.github/workflows/audit.yml b/.github/workflows/audit.yml
index bf852429459c..3ae9d192f376 100644
--- a/.github/workflows/audit.yml
+++ b/.github/workflows/audit.yml
@@ -16,7 +16,7 @@ jobs:
   audit:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: EmbarkStudios/cargo-deny-action@v1
         with:
           arguments: --all-features --workspace
diff --git a/.github/workflows/bench.yml b/.github/workflows/bench.yml
index 615a8ff6c0aa..ad0bbf81f2c2 100644
--- a/.github/workflows/bench.yml
+++ b/.github/workflows/bench.yml
@@ -30,14 +30,14 @@ jobs:
           echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV"
 
       - name: Check out Kani (old variant)
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: ./old
           ref: ${{ env.OLD_REF }}
           fetch-depth: 2
 
       - name: Check out Kani (new variant)
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: ./new
           ref: ${{ env.NEW_REF }}
diff --git a/.github/workflows/cbmc-latest.yml b/.github/workflows/cbmc-latest.yml
index 287215e554b7..9cb8082ae4b7 100644
--- a/.github/workflows/cbmc-latest.yml
+++ b/.github/workflows/cbmc-latest.yml
@@ -22,7 +22,7 @@ jobs:
         os: [macos-12, ubuntu-20.04, ubuntu-22.04]
     steps:
       - name: Checkout Kani under "kani"
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: kani
 
@@ -37,7 +37,7 @@ jobs:
         run: cargo build-dev
 
       - name: Checkout CBMC under "cbmc"
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           repository: diffblue/cbmc
           path: cbmc
@@ -58,7 +58,7 @@ jobs:
     runs-on: ubuntu-20.04
     steps:
       - name: Checkout Kani under "kani"
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: kani
 
@@ -73,7 +73,7 @@ jobs:
         run: cargo build-dev -- --release
 
       - name: Checkout CBMC under "cbmc"
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           repository: diffblue/cbmc
           path: cbmc
diff --git a/.github/workflows/cbmc-update.yml b/.github/workflows/cbmc-update.yml
index 3b8d6cbcd37e..e5f33e935e09 100644
--- a/.github/workflows/cbmc-update.yml
+++ b/.github/workflows/cbmc-update.yml
@@ -19,7 +19,7 @@ jobs:
     runs-on: ubuntu-22.04
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup
diff --git a/.github/workflows/extra_jobs.yml b/.github/workflows/extra_jobs.yml
index d4da80fbe132..45ca6968c4ba 100644
--- a/.github/workflows/extra_jobs.yml
+++ b/.github/workflows/extra_jobs.yml
@@ -33,7 +33,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - name: Checkout Kani
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
 
     - name: Label PR
       id: labeler
diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml
index 6a8267b09231..5ab7dcb1b9c3 100644
--- a/.github/workflows/format-check.yml
+++ b/.github/workflows/format-check.yml
@@ -14,7 +14,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Execute copyright check
         run: ./scripts/ci/run-copyright-check.sh
@@ -33,7 +33,7 @@ jobs:
     runs-on: ubuntu-20.04
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup
diff --git a/.github/workflows/kani-m1.yml b/.github/workflows/kani-m1.yml
index e9f973c82919..36f2b615c4aa 100644
--- a/.github/workflows/kani-m1.yml
+++ b/.github/workflows/kani-m1.yml
@@ -16,7 +16,7 @@ jobs:
     runs-on: macos-13-xlarge
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup
diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index a22ed971ec12..e866eaf635de 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -20,7 +20,7 @@ jobs:
         os: [macos-12, ubuntu-20.04, ubuntu-22.04]
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup
@@ -37,7 +37,7 @@ jobs:
     runs-on: ubuntu-20.04
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup
@@ -58,7 +58,7 @@ jobs:
     runs-on: ubuntu-20.04
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Install benchcomp dependencies
         run: |
@@ -81,7 +81,7 @@ jobs:
     runs-on: ubuntu-20.04
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup
@@ -102,7 +102,7 @@ jobs:
       contents: write
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index cdc69479d961..81bbf5959347 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -30,7 +30,7 @@ jobs:
       crate_version: ${{ steps.bundle.outputs.crate_version }}
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup
@@ -135,7 +135,7 @@ jobs:
           cargo kani setup --use-local-bundle ./${{ matrix.prev_job.bundle }}
 
       - name: Checkout tests
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Run tests
         # TODO: Customize compiletest to run custom kani. For now, just run a few cargo kani tests.
@@ -160,7 +160,7 @@ jobs:
       KANI_SRC: ./kani_src
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: ${{ env.KANI_SRC }}
 
@@ -204,7 +204,7 @@ jobs:
       upload_url: ${{ steps.create_release.outputs.upload_url }}
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Get version
         run: |
@@ -258,7 +258,7 @@ jobs:
       target: x86_64-unknown-linux-gnu
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup
diff --git a/.github/workflows/slow-tests.yml b/.github/workflows/slow-tests.yml
index 2c0a4acd9564..b177b6d5f400 100644
--- a/.github/workflows/slow-tests.yml
+++ b/.github/workflows/slow-tests.yml
@@ -21,7 +21,7 @@ jobs:
         os: [macos-12, ubuntu-20.04, ubuntu-22.04]
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup
diff --git a/.github/workflows/toolchain-upgrade.yml b/.github/workflows/toolchain-upgrade.yml
index 8d54ebe189ff..32266375cb5f 100644
--- a/.github/workflows/toolchain-upgrade.yml
+++ b/.github/workflows/toolchain-upgrade.yml
@@ -19,7 +19,7 @@ jobs:
     runs-on: ubuntu-22.04
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup

From 2475dc6b0f6c2eb3d835b3c604ff706b8cba7f84 Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Sat, 9 Dec 2023 15:00:27 +0100
Subject: [PATCH 5/5] Bump ncipollo/release-action from 1.12.0 to 1.13.0
 (#2919)

Bumps
[ncipollo/release-action](https://github.com/ncipollo/release-action)
from 1.12.0 to 1.13.0.
---
 .github/workflows/release.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 81bbf5959347..e753320c158f 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -235,7 +235,7 @@ jobs:
 
       - name: Create release
         id: create_release
-        uses: ncipollo/release-action@v1.12.0
+        uses: ncipollo/release-action@v1.13.0
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         with: