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 { 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,