Skip to content

Commit

Permalink
Merge branch 'main' into modifies_fat
Browse files Browse the repository at this point in the history
  • Loading branch information
pi314mm authored Jul 12, 2024
2 parents 202ca3a + 02e3327 commit 56f0d67
Show file tree
Hide file tree
Showing 4 changed files with 5 additions and 2 deletions.
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
2 changes: 2 additions & 0 deletions tests/expected/function-contract/const_fn_with_effect.rs
Original file line number Diff line number Diff line change
@@ -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.
//! <https://github.com/model-checking/kani/issues/3258>

#![feature(effects)]
#![allow(incomplete_features)]

#[kani::requires(kani::mem::can_dereference(arg))]
const unsafe fn dummy<T>(arg: *const T) -> T {
Expand Down
1 change: 1 addition & 0 deletions tools/compiletest/src/json.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down

0 comments on commit 56f0d67

Please sign in to comment.