diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs index 45670332a22f..1683147ce30e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -35,6 +35,7 @@ lazy_static! { "__rust_alloc_zeroed".into(), "__rust_dealloc".into(), "__rust_realloc".into(), + "__rust_no_alloc_shim_is_unstable_v2".into(), ]) }; } diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index 8efabb2c9517..b84420cb62b2 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -4,9 +4,10 @@ //! Module used to configure a compiler session. use crate::args::Arguments; +use rustc_driver::default_translator; use rustc_errors::{ - ColorConfig, DiagInner, emitter::Emitter, emitter::HumanReadableErrorType, - fallback_fluent_bundle, json::JsonEmitter, registry::Registry as ErrorRegistry, + ColorConfig, DiagInner, emitter::Emitter, emitter::HumanReadableErrorType, json::JsonEmitter, + registry::Registry as ErrorRegistry, }; use rustc_session::EarlyDiagCtxt; use rustc_session::config::ErrorOutputType; @@ -52,13 +53,11 @@ static JSON_PANIC_HOOK: LazyLock) + Sync + panic::set_hook(Box::new(|info| { // Print stack trace. let msg = format!("Kani unexpectedly panicked at {info}.",); - let fallback_bundle = - fallback_fluent_bundle(rustc_driver::DEFAULT_LOCALE_RESOURCES.to_vec(), false); let mut emitter = JsonEmitter::new( Box::new(io::BufWriter::new(io::stderr())), #[allow(clippy::arc_with_non_send_sync)] Some(Arc::new(SourceMap::new(FilePathMapping::empty()))), - fallback_bundle, + default_translator(), false, HumanReadableErrorType::Default, ColorConfig::Never, diff --git a/library/kani/kani_lib.c b/library/kani/kani_lib.c index 02a50708a7ff..1d25456fe08b 100644 --- a/library/kani/kani_lib.c +++ b/library/kani/kani_lib.c @@ -117,3 +117,9 @@ uint8_t *__rust_realloc(uint8_t *ptr, size_t old_size, size_t align, size_t new_ return result; } + +// Function required by the linker, see https://github.com/rust-lang/rust/pull/141061 +struct Unit __rust_no_alloc_shim_is_unstable_v2(void) +{ + return VoidUnit; +} diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 8779bc9606f9..b10626a86963 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-06-18" +channel = "nightly-2025-06-27" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]