Skip to content

Commit

Permalink
Update toolchain to nightly-2023-08-24 (model-checking#2711)
Browse files Browse the repository at this point in the history
Changes were required due to:

- rust-lang/rust#115011
- rust-lang/rust#114993
  • Loading branch information
celinval authored and tautschnig committed Aug 30, 2023
1 parent 4d84ff4 commit ed26d59
Show file tree
Hide file tree
Showing 5 changed files with 10 additions and 10 deletions.
6 changes: 3 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
Original file line number Diff line number Diff line change
Expand Up @@ -118,13 +118,13 @@ impl<'tcx> GotocCtx<'tcx> {
// because we don't want to raise the warning during compilation.
// These operations will normally be codegen'd but normally be unreachable
// since we make use of `-C unwind=abort`.
TerminatorKind::Resume => self.codegen_mimic_unimplemented(
TerminatorKind::UnwindResume => self.codegen_mimic_unimplemented(
"TerminatorKind::Resume",
loc,
"https://github.com/model-checking/kani/issues/692",
),
TerminatorKind::Terminate => self.codegen_mimic_unimplemented(
"TerminatorKind::Terminate",
TerminatorKind::UnwindTerminate => self.codegen_mimic_unimplemented(
"TerminatorKind::UnwindTerminate",
loc,
"https://github.com/model-checking/kani/issues/692",
),
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/analysis.rs
Original file line number Diff line number Diff line change
Expand Up @@ -157,10 +157,10 @@ impl<'tcx> From<&Terminator<'tcx>> for Key {
TerminatorKind::FalseEdge { .. } => Key("FalseEdge"),
TerminatorKind::FalseUnwind { .. } => Key("FalseUnwind"),
TerminatorKind::InlineAsm { .. } => Key("InlineAsm"),
TerminatorKind::Resume => Key("Resume"),
TerminatorKind::UnwindResume => Key("UnwindResume"),
TerminatorKind::Return => Key("Return"),
TerminatorKind::SwitchInt { .. } => Key("SwitchInt"),
TerminatorKind::Terminate => Key("Terminate"),
TerminatorKind::UnwindTerminate => Key("UnwindTerminate"),
TerminatorKind::Unreachable => Key("Unreachable"),
TerminatorKind::Yield { .. } => Key("Yield"),
}
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/reachability.rs
Original file line number Diff line number Diff line change
Expand Up @@ -532,12 +532,12 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> {
// We don't support inline assembly. This shall be replaced by an unsupported
// construct during codegen.
}
TerminatorKind::Terminate { .. } | TerminatorKind::Assert { .. } => {
TerminatorKind::UnwindTerminate { .. } | TerminatorKind::Assert { .. } => {
// We generate code for this without invoking any lang item.
}
TerminatorKind::Goto { .. }
| TerminatorKind::SwitchInt { .. }
| TerminatorKind::Resume
| TerminatorKind::UnwindResume
| TerminatorKind::Return
| TerminatorKind::Unreachable => {}
TerminatorKind::GeneratorDrop
Expand Down
4 changes: 2 additions & 2 deletions kani-driver/src/cbmc_output_parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -95,8 +95,8 @@ pub struct PropertyId {
}

impl Property {
const COVER_PROPERTY_CLASS: &str = "cover";
const COVERAGE_PROPERTY_CLASS: &str = "code_coverage";
const COVER_PROPERTY_CLASS: &'static str = "cover";
const COVERAGE_PROPERTY_CLASS: &'static str = "code_coverage";

pub fn property_class(&self) -> String {
self.property_id.class.clone()
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-2023-08-19"
channel = "nightly-2023-08-24"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

0 comments on commit ed26d59

Please sign in to comment.