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"]