Skip to content

Commit 8ccdea4

Browse files
authored
Update toolchain to nightly-2023-08-24 (#2711)
Changes were required due to: - rust-lang/rust#115011 - rust-lang/rust#114993
1 parent 5516650 commit 8ccdea4

File tree

5 files changed

+10
-10
lines changed

5 files changed

+10
-10
lines changed

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

+3-3
Original file line numberDiff line numberDiff line change
@@ -118,13 +118,13 @@ impl<'tcx> GotocCtx<'tcx> {
118118
// because we don't want to raise the warning during compilation.
119119
// These operations will normally be codegen'd but normally be unreachable
120120
// since we make use of `-C unwind=abort`.
121-
TerminatorKind::Resume => self.codegen_mimic_unimplemented(
121+
TerminatorKind::UnwindResume => self.codegen_mimic_unimplemented(
122122
"TerminatorKind::Resume",
123123
loc,
124124
"https://github.com/model-checking/kani/issues/692",
125125
),
126-
TerminatorKind::Terminate => self.codegen_mimic_unimplemented(
127-
"TerminatorKind::Terminate",
126+
TerminatorKind::UnwindTerminate => self.codegen_mimic_unimplemented(
127+
"TerminatorKind::UnwindTerminate",
128128
loc,
129129
"https://github.com/model-checking/kani/issues/692",
130130
),

kani-compiler/src/kani_middle/analysis.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -157,10 +157,10 @@ impl<'tcx> From<&Terminator<'tcx>> for Key {
157157
TerminatorKind::FalseEdge { .. } => Key("FalseEdge"),
158158
TerminatorKind::FalseUnwind { .. } => Key("FalseUnwind"),
159159
TerminatorKind::InlineAsm { .. } => Key("InlineAsm"),
160-
TerminatorKind::Resume => Key("Resume"),
160+
TerminatorKind::UnwindResume => Key("UnwindResume"),
161161
TerminatorKind::Return => Key("Return"),
162162
TerminatorKind::SwitchInt { .. } => Key("SwitchInt"),
163-
TerminatorKind::Terminate => Key("Terminate"),
163+
TerminatorKind::UnwindTerminate => Key("UnwindTerminate"),
164164
TerminatorKind::Unreachable => Key("Unreachable"),
165165
TerminatorKind::Yield { .. } => Key("Yield"),
166166
}

kani-compiler/src/kani_middle/reachability.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -532,12 +532,12 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> {
532532
// We don't support inline assembly. This shall be replaced by an unsupported
533533
// construct during codegen.
534534
}
535-
TerminatorKind::Terminate { .. } | TerminatorKind::Assert { .. } => {
535+
TerminatorKind::UnwindTerminate { .. } | TerminatorKind::Assert { .. } => {
536536
// We generate code for this without invoking any lang item.
537537
}
538538
TerminatorKind::Goto { .. }
539539
| TerminatorKind::SwitchInt { .. }
540-
| TerminatorKind::Resume
540+
| TerminatorKind::UnwindResume
541541
| TerminatorKind::Return
542542
| TerminatorKind::Unreachable => {}
543543
TerminatorKind::GeneratorDrop

kani-driver/src/cbmc_output_parser.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -95,8 +95,8 @@ pub struct PropertyId {
9595
}
9696

9797
impl Property {
98-
const COVER_PROPERTY_CLASS: &str = "cover";
99-
const COVERAGE_PROPERTY_CLASS: &str = "code_coverage";
98+
const COVER_PROPERTY_CLASS: &'static str = "cover";
99+
const COVERAGE_PROPERTY_CLASS: &'static str = "code_coverage";
100100

101101
pub fn property_class(&self) -> String {
102102
self.property_id.class.clone()

rust-toolchain.toml

+1-1
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-08-19"
5+
channel = "nightly-2023-08-24"
66
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

0 commit comments

Comments
 (0)