Skip to content

Commit a8a2346

Browse files
authored
Update Rust toolchain to 2023-11-06 (#2858)
Update to the latest Rust toolchain (2023-11-06). The relevant changes are: - rust-lang/rust#117507: this required changing the import of `Span` from `rustc_span::source_map::Span` to `rustc_span::Span`. - rust-lang/rust#114208: this changed the data field for the `OffsetOf` variant of `NullOp` from `List<FieldIdx>` to `List<(VariantIdx, FieldIdx)>`, which required updating the relevant code in `rvalue.rs`. - rust-lang/rust#115626: the unchecked shift operators have been separated from the `unchecked_math` feature, so this required changing the feature annotation in `tests/ui/should-panic-attribute/unexpected-failures/test.rs` - Some rustc change (not sure which one) result in a line in `tests/coverage/unreachable/variant/main.rs` getting optimized out. To maintain what this test is testing, I changed the `match` to make it a bit less-prone to optimization. - A change in `cargo` (rust-lang/cargo#12779) resulted in an update to Kani's workspace `Cargo.toml` when `cargo add` is executed inside `tests/script-based-pre/build-cache-bin`. This is apparently intended behavior, so I had to make the `exclude` in the `Cargo.toml` more specific to make sure this doesn't happen (I tried using a glob, but that didn't work, apparently because of rust-lang/cargo#6009. Resolves #2848 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 6cb6526 commit a8a2346

File tree

7 files changed

+10
-7
lines changed

7 files changed

+10
-7
lines changed

Cargo.toml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -67,4 +67,6 @@ exclude = [
6767
"tests/slow",
6868
"tests/assess-scan-test-scaffold",
6969
"tests/script-based-pre",
70+
"tests/script-based-pre/build-cache-bin/target/new_dep",
71+
"tests/script-based-pre/build-cache-dirty/target/new_dep",
7072
]

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -727,7 +727,7 @@ impl<'tcx> GotocCtx<'tcx> {
727727
.with_size_of_annotation(self.codegen_ty(t)),
728728
NullOp::AlignOf => Expr::int_constant(layout.align.abi.bytes(), Type::size_t()),
729729
NullOp::OffsetOf(fields) => Expr::int_constant(
730-
layout.offset_of_subfield(self, fields.iter().map(|f| f.index())).bytes(),
730+
layout.offset_of_subfield(self, fields.iter()).bytes(),
731731
Type::size_t(),
732732
),
733733
}

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,8 @@ use rustc_middle::ty::layout::{
3131
TyAndLayout,
3232
};
3333
use rustc_middle::ty::{self, Instance, Ty, TyCtxt};
34-
use rustc_span::source_map::{respan, Span};
34+
use rustc_span::source_map::respan;
35+
use rustc_span::Span;
3536
use rustc_target::abi::call::FnAbi;
3637
use rustc_target::abi::{HasDataLayout, TargetDataLayout};
3738

rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2023-10-31"
5+
channel = "nightly-2023-11-06"
66
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

tests/coverage/unreachable/variant/expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
coverage/unreachable/variant/main.rs, 15, FULL
1+
coverage/unreachable/variant/main.rs, 15, PARTIAL
22
coverage/unreachable/variant/main.rs, 16, NONE
33
coverage/unreachable/variant/main.rs, 17, NONE
44
coverage/unreachable/variant/main.rs, 18, FULL

tests/coverage/unreachable/variant/main.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,9 @@ fn print_direction(dir: Direction) {
1616
Direction::Up => println!("Going up!"),
1717
Direction::Down => println!("Going down!"),
1818
Direction::Left => println!("Going left!"),
19-
Direction::Right => println!("Going right!"),
19+
Direction::Right if 1 == 1 => println!("Going right!"),
2020
// This part is unreachable since we cover all variants in the match.
21-
_ => {}
21+
_ => println!("Not going anywhere!"),
2222
}
2323
}
2424

tests/ui/should-panic-attribute/unexpected-failures/test.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33

44
//! Checks that verfication fails when `#[kani::should_panic]` is used but not
55
//! all failures encountered are panics.
6-
#![feature(unchecked_math)]
6+
#![feature(unchecked_shifts)]
77

88
fn trigger_overflow() {
99
let x: u32 = kani::any();

0 commit comments

Comments
 (0)