Update toolchain to 2025-04-14

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

@@ -813,7 +813,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             let disambiguator = CharonDisambiguator::new(data.disambiguator as usize);
             use rustc_hir::definitions::DefPathData;
             match &data.data {
-                DefPathData::TypeNs(Some(symbol)) => {
+                DefPathData::TypeNs(symbol) => {
                     error_assert!(self, span, data.disambiguator == 0); // Sanity check
                     name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator));
                 }
@@ -956,7 +956,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             let disambiguator = CharonDisambiguator::new(data.disambiguator as usize);
             use rustc_hir::definitions::DefPathData;
             match &data.data {
-                DefPathData::TypeNs(Some(symbol)) => {
+                DefPathData::TypeNs(symbol) => {
                     error_assert!(self, span, data.disambiguator == 0); // Sanity check
                     name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator));
                 }
@@ -1063,7 +1063,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             let disambiguator = CharonDisambiguator::new(data.disambiguator as usize);
             use rustc_hir::definitions::DefPathData;
             match &data.data {
-                DefPathData::TypeNs(Some(symbol)) => {
+                DefPathData::TypeNs(symbol) => {
                     error_assert!(self, span, data.disambiguator == 0); // Sanity check
                     name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator));
                 }

rust-toolchain.toml

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

tests/expected/uninit/intrinsics/expected

@@ -1,7 +1,3 @@
-std::ptr::read::<std::mem::MaybeUninit<u8>>.unsupported_construct.\
-	 - Status: FAILURE\
-	 - Description: "Interaction between raw pointers and unions is not yet supported."
-
 check_typed_swap_nonoverlapping.safety_check.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`"

tests/kani/FunctionContracts/modify_slice_elem.rs → tests/kani/FunctionContracts/modify_slice_elem_fixme.rs

@@ -2,6 +2,9 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! Check that Kani correctly verifies the contract that modifies slices.
 //!
+//! This started failing with the 2025-04-05 toolchain upgrade
+//! Tracking issue: https://github.com/model-checking/kani/issues/4029
+//!
 //! Note that this test used to crash while parsing the annotations.
 // kani-flags: -Zfunction-contracts
 extern crate kani;

tests/perf/smol_str/src/lib.rs

@@ -5,9 +5,11 @@
 //! <https://github.com/model-checking/kani/issues/3312>
 
 #[kani::proof]
-#[kani::unwind(4)]
+#[kani::unwind(13)]
 fn check_new() {
-    let data: [char; 3] = kani::any();
-    let input: String = data.iter().collect();
+    let data: [u8; 12] = kani::any();
+    let res = String::from_utf8(data.into());
+    kani::assume(res.is_ok());
+    let input: String = res.unwrap();
     smol_str::SmolStr::new(&input);
 }