Skip to content

Commit

Permalink
Update the rust toolchain to nightly-2024-06-04
Browse files Browse the repository at this point in the history
Changes required due to:
- rust-lang/rust@a34c26e7ec Make body_owned_by return the body directly.
- rust-lang/rust@333458c2cb Uplift TypeRelation and Relate
- rust-lang/rust@459ce3f6bb Add an intrinsic for `ptr::metadata`

Resolves: model-checking#3218
  • Loading branch information
tautschnig committed Jun 4, 2024
1 parent 7bf23a2 commit 741b401
Show file tree
Hide file tree
Showing 4 changed files with 10 additions and 4 deletions.
6 changes: 6 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -799,6 +799,12 @@ impl<'tcx> GotocCtx<'tcx> {
}
}
UnOp::Neg => self.codegen_operand_stable(e).neg(),
UnOp::PtrMetadata => {
// 1. create a test that uses std::ptr::metadata
// 2. figure out what the operand is (should be a raw ptr)
// 3. figure out what res_ty is
todo!()
}
},
Rvalue::Discriminant(p) => {
let place =
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,8 @@ use rustc_middle::ty::print::with_no_trimmed_paths;
use rustc_middle::ty::print::FmtPrinter;
use rustc_middle::ty::GenericArgsRef;
use rustc_middle::ty::{
self, AdtDef, Const, CoroutineArgs, FloatTy, Instance, IntTy, PolyFnSig, Ty, TyCtxt, TyKind,
UintTy, VariantDef, VtblEntry,
self, AdtDef, Const, CoroutineArgs, CoroutineArgsExt, FloatTy, Instance, IntTy, PolyFnSig, Ty,
TyCtxt, TyKind, UintTy, VariantDef, VtblEntry,
};
use rustc_middle::ty::{List, TypeFoldable};
use rustc_smir::rustc_internal;
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/attributes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -632,7 +632,7 @@ fn parse_modify_values<'a>(
TokenTree::Token(token, _) => {
if let TokenKind::Ident(id, _) = &token.kind {
let hir = tcx.hir();
let bid = hir.body_owned_by(local_def_id);
let bid = hir.body_owned_by(local_def_id).id();
Some(
hir.body_param_names(bid)
.zip(mir.args_iter())
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-05-28"
channel = "nightly-2024-06-04"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

0 comments on commit 741b401

Please sign in to comment.