Update to today's toolchain (2023-08-24)

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",
             ),

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"),
         }

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

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()

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