diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index d0f41ca0e2dc..93a394aad326 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -27,6 +27,7 @@ use clap::Parser; use rustc_codegen_ssa::traits::CodegenBackend; use rustc_driver::{Callbacks, Compilation, RunCompiler}; use rustc_interface::Config; +use rustc_middle::ty::TyCtxt; use rustc_session::config::ErrorOutputType; use rustc_smir::rustc_internal; use rustc_span::ErrorGuaranteed; @@ -124,17 +125,15 @@ impl Callbacks for KaniCompiler { } /// After analysis, we check the crate items for Kani API misuse or configuration issues. - fn after_analysis<'tcx>( + fn after_analysis( &mut self, _compiler: &rustc_interface::interface::Compiler, - rustc_queries: &'tcx rustc_interface::Queries<'tcx>, + tcx: TyCtxt<'_>, ) -> Compilation { - rustc_queries.global_ctxt().unwrap().enter(|tcx| { - rustc_internal::run(tcx, || { - check_crate_items(tcx, self.queries.lock().unwrap().args().ignore_global_asm); - }) - .unwrap() - }); + rustc_internal::run(tcx, || { + check_crate_items(tcx, self.queries.lock().unwrap().args().ignore_global_asm); + }) + .unwrap(); Compilation::Continue } } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index c699ced8a0ab..017266717de7 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -673,12 +673,12 @@ fn expect_key_string_value( attr: &Attribute, ) -> Result { let span = attr.span; - let AttrArgs::Eq(_, it) = &attr.get_normal_item().args else { + let AttrArgs::Eq { eq_span: _, value } = &attr.get_normal_item().args else { return Err(sess .dcx() .span_err(span, "Expected attribute of the form #[attr = \"value\"]")); }; - let maybe_str = match it { + let maybe_str = match value { AttrArgsEq::Ast(expr) => { if let ExprKind::Lit(tok) = expr.kind { match LitKind::from_token_lit(tok) { diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index 0af517ca84bc..da04cc0517ba 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -76,7 +76,7 @@ impl Project { trace!(?harness.goto_file, ?expected_path, ?typ, "get_harness_artifact"); self.artifacts.iter().find(|artifact| { artifact.has_type(typ) - && expected_path.as_ref().map_or(true, |goto_file| *goto_file == artifact.path) + && expected_path.as_ref().is_none_or(|goto_file| *goto_file == artifact.path) }) } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 9d51f9566f61..b49477fe680a 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-11-28" +channel = "nightly-2024-12-09" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/llbc/enum/expected b/tests/expected/llbc/enum/expected index 10409fdab8e8..9d35f16b5205 100644 --- a/tests/expected/llbc/enum/expected +++ b/tests/expected/llbc/enum/expected @@ -29,7 +29,7 @@ fn test::main() let i@2: i32; // local e@1 := test::MyEnum::A { 0: const (1 : i32) } - i@2 := @Fun1(move (e@1)) + i@2 := @Fun0(move (e@1)) drop i@2 @0 := () return diff --git a/tests/expected/llbc/generic/expected b/tests/expected/llbc/generic/expected index c0ef3c1939e0..8345efd371d4 100644 --- a/tests/expected/llbc/generic/expected +++ b/tests/expected/llbc/generic/expected @@ -43,7 +43,7 @@ fn test::main() @2 := core::option::Option::Some { 0: const (1 : i32) } @3 := core::option::Option::Some { 0: const (2 : i32) } - e@1 := @Fun1(move (@2), move (@3)) + e@1 := @Fun0(move (@2), move (@3)) drop @3 drop @2 drop e@1 diff --git a/tests/expected/llbc/projection/expected b/tests/expected/llbc/projection/expected index 378fef9659c6..5753b9f18170 100644 --- a/tests/expected/llbc/projection/expected +++ b/tests/expected/llbc/projection/expected @@ -4,18 +4,19 @@ struct test::MyStruct = b: i32, } enum test::MyEnum0 = -| A(0: @Adt0, 1: i32) +| A(0: @Adt1, 1: i32) | B() enum test::MyEnum = -| A(0: @Adt0, 1: @Adt2) +| A(0: @Adt1, 1: @Adt2) | B(0: (i32, i32)) -fn test::enum_match(@1: @Adt1) -> i32 + +fn test::enum_match(@1: @Adt0) -> i32 { let @0: i32; // return - let e@1: @Adt1; // arg #1 - let s@2: @Adt0; // local + let e@1: @Adt0; // arg #1 + let s@2: @Adt1; // local let e0@3: @Adt2; // local - let s1@4: @Adt0; // local + let s1@4: @Adt1; // local let b@5: i32; // local let @6: i32; // anonymous local let @7: i32; // anonymous local @@ -59,17 +60,18 @@ fn test::enum_match(@1: @Adt1) -> i32 fn test::main() { let @0: (); // return - let s@1: @Adt0; // local - let s0@2: @Adt0; // local - let e@3: @Adt1; // local + let s@1: @Adt1; // local + let s0@2: @Adt1; // local + let e@3: @Adt0; // local let @4: @Adt2; // anonymous local let i@5: i32; // local - s@1 := @Adt0 { a: const (1 : i32), b: const (2 : i32) } - s0@2 := @Adt0 { a: const (1 : i32), b: const (2 : i32) } + s@1 := @Adt1 { a: const (1 : i32), b: const (2 : i32) } + s0@2 := @Adt1 { a: const (1 : i32), b: const (2 : i32) } + @4 := test::MyEnum0::A { 0: move (s0@2), 1: const (1 : i32) } e@3 := test::MyEnum::A { 0: move (s@1), 1: move (@4) } drop @4 - i@5 := @Fun1(move (e@3)) + i@5 := @Fun0(move (e@3)) drop i@5 @0 := () return diff --git a/tests/expected/llbc/tuple/expected b/tests/expected/llbc/tuple/expected index 1475d136b7cc..d6fa6330ca88 100644 --- a/tests/expected/llbc/tuple/expected +++ b/tests/expected/llbc/tuple/expected @@ -20,7 +20,7 @@ fn test::main() let @2: (i32, i32); // anonymous local @2 := (const (1 : i32), const (2 : i32)) - s@1 := @Fun1(move (@2)) + s@1 := @Fun0(move (@2)) drop @2 drop s@1 @0 := ()