From 5f8bef5ce4a4c47d4c643666abfbf4be5653c2b8 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 24 Aug 2023 12:21:19 -0700 Subject: [PATCH] Update to today's toolchain (2023-08-24) --- .../src/codegen_cprover_gotoc/codegen/statement.rs | 6 +++--- kani-compiler/src/kani_middle/analysis.rs | 4 ++-- kani-compiler/src/kani_middle/reachability.rs | 4 ++-- kani-driver/src/cbmc_output_parser.rs | 4 ++-- rust-toolchain.toml | 2 +- 5 files changed, 10 insertions(+), 10 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index fbabe7e112cd..a7b49170bd3f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -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", ), diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index ee0b8e769bc7..ada4eca63859 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -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"), } diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 7f1daf98ecca..466bad80e569 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -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 diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index 8bdd45034190..1bb353d7d4c0 100644 --- a/kani-driver/src/cbmc_output_parser.rs +++ b/kani-driver/src/cbmc_output_parser.rs @@ -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() diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 44d74d303ef8..8cfec028bae1 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -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"]