From ada9720a32067f8188642adf23e47c65f6aaded1 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 12 Jul 2024 17:55:07 +0000 Subject: [PATCH 1/2] Move to 7/12 --- kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs | 2 +- rust-toolchain.toml | 2 +- tests/expected/function-contract/const_fn_with_effect.rs | 2 ++ 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 6e6547295ff9..1703335dda51 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -574,7 +574,7 @@ impl<'tcx> GotocCtx<'tcx> { ty::Ref(_, t, _) | ty::RawPtr(t, _) => self.codegen_ty_ref(*t), ty::FnDef(def_id, args) => { let instance = - Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args) + Instance::try_resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args) .unwrap() .unwrap(); self.codegen_fndef_type(instance) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index dfe3febbb927..f2e8fede457c 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-07-01" +channel = "nightly-2024-07-12" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/function-contract/const_fn_with_effect.rs b/tests/expected/function-contract/const_fn_with_effect.rs index d57c1f42fe16..070c44482a80 100644 --- a/tests/expected/function-contract/const_fn_with_effect.rs +++ b/tests/expected/function-contract/const_fn_with_effect.rs @@ -1,11 +1,13 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -Zmem-predicates +// compile-flags: -Znext-solver //! Check that Kani contract can be applied to a constant function. //! #![feature(effects)] +#![allow(incomplete_features)] #[kani::requires(kani::mem::can_dereference(arg))] const unsafe fn dummy(arg: *const T) -> T { From 959dc55dca8a09389245ec1d7d601381b7ede333 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 12 Jul 2024 18:34:14 +0000 Subject: [PATCH 2/2] Fix clippy warning --- tools/compiletest/src/json.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/tools/compiletest/src/json.rs b/tools/compiletest/src/json.rs index c46c3b3225e8..89c733abc59a 100644 --- a/tools/compiletest/src/json.rs +++ b/tools/compiletest/src/json.rs @@ -35,6 +35,7 @@ struct FutureBreakageItem { } #[derive(Deserialize, Clone)] +#[allow(dead_code)] struct DiagnosticSpanMacroExpansion { /// name of macro that was applied (e.g., "foo!" or "#[derive(Eq)]") _macro_decl_name: String,