Fix the merge

Author: celinval

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

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 {

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)

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