From a6f00a003b5c4c787984d207917adc283a3a7720 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Thu, 4 May 2023 11:26:30 -0700
Subject: [PATCH] Fix the merge

---
 kani-compiler/src/kani_middle/analysis.rs       | 4 ++--
 kani-compiler/src/kani_middle/attributes.rs     | 5 +++++
 tests/cargo-ui/unstable-attr/invalid/expected   | 6 +++---
 tests/cargo-ui/unstable-attr/invalid/src/lib.rs | 5 +++++
 4 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs
index e618d8ec2163..ee0b8e769bc7 100644
--- a/kani-compiler/src/kani_middle/analysis.rs
+++ b/kani-compiler/src/kani_middle/analysis.rs
@@ -138,6 +138,7 @@ impl<'tcx> From<&Statement<'tcx>> for Key {
             | StatementKind::ConstEvalCounter
             | StatementKind::FakeRead(_)
             | StatementKind::Nop
+            | StatementKind::PlaceMention(_)
             | StatementKind::Retag(_, _)
             | StatementKind::StorageLive(_)
             | StatementKind::StorageDead(_) => Key("Ignored"),
@@ -148,11 +149,9 @@ impl<'tcx> From<&Statement<'tcx>> for Key {
 impl<'tcx> From<&Terminator<'tcx>> for Key {
     fn from(value: &Terminator<'tcx>) -> Self {
         match value.kind {
-            TerminatorKind::Abort => Key("Abort"),
             TerminatorKind::Assert { .. } => Key("Assert"),
             TerminatorKind::Call { .. } => Key("Call"),
             TerminatorKind::Drop { .. } => Key("Drop"),
-            TerminatorKind::DropAndReplace { .. } => Key("DropAndReplace"),
             TerminatorKind::GeneratorDrop => Key("GeneratorDrop"),
             TerminatorKind::Goto { .. } => Key("Goto"),
             TerminatorKind::FalseEdge { .. } => Key("FalseEdge"),
@@ -161,6 +160,7 @@ impl<'tcx> From<&Terminator<'tcx>> for Key {
             TerminatorKind::Resume => Key("Resume"),
             TerminatorKind::Return => Key("Return"),
             TerminatorKind::SwitchInt { .. } => Key("SwitchInt"),
+            TerminatorKind::Terminate => Key("Terminate"),
             TerminatorKind::Unreachable => Key("Unreachable"),
             TerminatorKind::Yield { .. } => Key("Yield"),
         }
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 8bb298dbd810..577697793b4d 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -155,6 +155,11 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> Option<HarnessA
 ///
 /// TODO: Improve error message by printing the span of the callee instead of the definition.
 pub fn check_unstable_features(tcx: TyCtxt, enabled_features: &[String], def_id: DefId) {
+    if !matches!(tcx.type_of(def_id).0.kind(), TyKind::FnDef(..)) {
+        // skip closures due to an issue with rustc.
+        // https://github.com/model-checking/kani/pull/2406#issuecomment-1534333862
+        return;
+    }
     let attributes = extract_kani_attributes(tcx, def_id);
     if let Some(unstable_attrs) = attributes.get(&KaniAttributeKind::Unstable) {
         for attr in unstable_attrs {
diff --git a/tests/cargo-ui/unstable-attr/invalid/expected b/tests/cargo-ui/unstable-attr/invalid/expected
index 66d0c5271668..b3acac173184 100644
--- a/tests/cargo-ui/unstable-attr/invalid/expected
+++ b/tests/cargo-ui/unstable-attr/invalid/expected
@@ -1,8 +1,8 @@
-error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `feature("invalid_args")`\
+error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found\
 src/lib.rs\
 |\
-| #[kani::unstable(feature("invalid_args"))]\
-| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
+| #[kani::unstable(\
+| ^^^^^^^^^^^^^^^^^^\
 |\
 = note: expected format: #[kani::unstable(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]\
 = note: this error originates in the attribute macro `kani::unstable` (in Nightly builds, run with -Z macro-backtrace for more info)
diff --git a/tests/cargo-ui/unstable-attr/invalid/src/lib.rs b/tests/cargo-ui/unstable-attr/invalid/src/lib.rs
index f6f55bc112ef..5fbfc768c883 100644
--- a/tests/cargo-ui/unstable-attr/invalid/src/lib.rs
+++ b/tests/cargo-ui/unstable-attr/invalid/src/lib.rs
@@ -1,6 +1,11 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+//! All the unstable definitions below should fail.
+//! The expected file only contains a generic check since we trigger an ICE for debug builds and
+//! we don't guarantee the order that these will be evaluated.
+//! TODO: We should break down this test to ensure all of these fail.
+
 #[kani::unstable(reason = "just checking", issue = "<link>")]
 pub fn missing_feature() {
     todo!()