Update toolchain to 2/5

- Regression for delayed UB for slices: rust-lang/rust#135265

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-02-04"
+channel = "nightly-2025-02-05"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/expected/uninit/delayed-ub/expected → tests/expected/uninit/delayed-ub/delayed-ub.expected

@@ -2,10 +2,6 @@ delayed_ub_trigger_copy.assertion.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\
 
-delayed_ub_slices.assertion.\
-	 - Status: FAILURE\
-	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`"
-
 delayed_ub_structs.assertion.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `U`"
@@ -44,7 +40,6 @@ delayed_ub.assertion.\
 
 Summary:
 Verification failed for - delayed_ub_trigger_copy
-Verification failed for - delayed_ub_slices
 Verification failed for - delayed_ub_structs
 Verification failed for - delayed_ub_double_copy
 Verification failed for - delayed_ub_copy
@@ -54,4 +49,4 @@ Verification failed for - delayed_ub_laundered
 Verification failed for - delayed_ub_static
 Verification failed for - delayed_ub_transmute
 Verification failed for - delayed_ub
-Complete - 0 successfully verified harnesses, 11 failures, 11 total.
+Complete - 0 successfully verified harnesses, 10 failures, 10 total.

tests/expected/uninit/delayed-ub/delayed-ub.rs

@@ -170,19 +170,6 @@ fn delayed_ub_structs() {
     }
 }
 
-/// Delayed UB via mutable pointer write into a slice element.
-#[kani::proof]
-fn delayed_ub_slices() {
-    unsafe {
-        // Create an array.
-        let mut arr = [0u128; 4];
-        // Get a pointer to a part of the array.
-        let ptr = &mut arr[0..2][0..1][0] as *mut _ as *mut (u8, u32);
-        *ptr = (4, 4);
-        let arr_copy = arr; // UB: This reads a padding value inside the array!
-    }
-}
-
 /// Delayed UB via mutable pointer copy, which should be the only delayed UB trigger in this case.
 #[kani::proof]
 fn delayed_ub_trigger_copy() {

tests/expected/uninit/delayed-ub/slices_fixme.expected

@@ -0,0 +1,5 @@
+delayed_ub_slices.assertion.\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`"
+
+Verification failed for - delayed_ub_slices

tests/expected/uninit/delayed-ub/slices_fixme.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z ghost-state -Z uninit-checks
+
+//! Checks that Kani catches instances of delayed UB for slices.
+//! This test used to live inside delayed-ub, but the 2/5/2025 toolchain upgrade introduced a regression for this test.
+//! Once this test is fixed, move it back into delayed-ub.rs
+//! See https://github.com/model-checking/kani/issues/3881 for details.
+
+/// Delayed UB via mutable pointer write into a slice element.
+#[kani::proof]
+fn delayed_ub_slices() {
+    unsafe {
+        // Create an array.
+        let mut arr = [0u128; 4];
+        // Get a pointer to a part of the array.
+        let ptr = &mut arr[0..2][0..1][0] as *mut _ as *mut (u8, u32);
+        *ptr = (4, 4);
+        let arr_copy = arr; // UB: This reads a padding value inside the array!
+    }
+}