More error handling, improve UI testing

library/kani_macros/src/derive.rs

@@ -274,7 +274,7 @@ fn parse_safety_expr(ident: &Ident, field: &syn::Field) -> Option<TokenStream> {
     }
 }
 
-fn parse_safety_expr_struct(ident: &Ident, derive_input: &DeriveInput) -> Option<TokenStream> {
+fn parse_safety_expr_input(ident: &Ident, derive_input: &DeriveInput) -> Option<TokenStream> {
     let name = ident;
     let mut safety_attr = None;
 
@@ -407,8 +407,9 @@ fn safety_conds_opt(
     derive_input: &DeriveInput,
     trait_name: &str,
 ) -> Option<TokenStream> {
-    let has_item_safety_constraint = has_item_safety_constraint(&item_name, &derive_input, trait_name);
-
+    let has_item_safety_constraint =
+        has_item_safety_constraint(&item_name, &derive_input, trait_name);
+
     let has_field_safety_constraints = has_field_safety_constraints(&item_name, &derive_input.data);
 
     if has_item_safety_constraint && has_field_safety_constraints {
@@ -428,7 +429,8 @@ fn safety_conds_opt(
 }
 
 fn has_item_safety_constraint(ident: &Ident, derive_input: &DeriveInput, trait_name: &str) -> bool {
-    let safety_constraints_in_item = derive_input.attrs.iter().filter(|attr| attr.path().is_ident("safety_constraint")).count();
+    let safety_constraints_in_item =
+        derive_input.attrs.iter().filter(|attr| attr.path().is_ident("safety_constraint")).count();
     if safety_constraints_in_item > 1 {
         abort!(Span::call_site(), "Cannot derive `{}` for `{}`", trait_name, ident;
         note = ident.span() =>
@@ -472,10 +474,15 @@ pub fn add_trait_bound_invariant(mut generics: Generics) -> Generics {
 fn safe_body_from_struct_attr(
     ident: &Ident,
     derive_input: &DeriveInput,
-    _trait_name: &str,
+    trait_name: &str,
 ) -> TokenStream {
-    // TODO: Check that this is a struct
-    parse_safety_expr_struct(ident, derive_input).unwrap()
+    if !matches!(derive_input.data, Data::Struct(_)) {
+        abort!(Span::call_site(), "Cannot derive `{}` for `{}`", trait_name, ident;
+            note = ident.span() =>
+            "`#[safety_constraint(...)]` can only be used in structs"
+        )
+    };
+    parse_safety_expr_input(ident, derive_input).unwrap()
 }
 
 /// Parse the condition expressions in `#[safety_constraint(<cond>)]` attached to struct

tests/ui/attr-invariant/invalid-pred-error/invalid-pred-error.rs → tests/ui/safety-constraint-attribute/invalid-pred-error/invalid-pred-error.rs

@@ -1,9 +1,10 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! Check that there is a compilation error when the predicate passed to
+//! Check that there is a compilation error when the predicate passed to the
 //! `#[safety_constraint(...)]` attribute would result in a compiler error.
-//! The `#[derive(kani::Invariant)]` macro is required for the compiler error,
+//!
+//! Note: the `#[derive(kani::Invariant)]` macro is required for the compiler error,
 //! otherwise the `#[safety_constraint(...)]` attribute is ignored.
 
 extern crate kani;

tests/ui/safety-constraint-attribute/no-struct-error/expected

@@ -0,0 +1,6 @@
+error: Cannot derive `Invariant` for `MyEnum`
+   |
+| #[derive(kani::Invariant)]
+   |          ^^^^^^^^^^^^^^^
+   |
+note: `#[safety_constraint(...)]` can only be used in structs

tests/ui/safety-constraint-attribute/no-struct-error/no-struct-error.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that Kani raises an error when a derive macro with the
+//! `#[safety_constraint(...)]` attribute is is used in items which are not a
+//! struct.
+//!
+//! Note: the `#[derive(kani::Invariant)]` macro is required for the compiler error,
+//! otherwise the `#[safety_constraint(...)]` attribute is ignored.
+
+extern crate kani;
+
+#[derive(kani::Invariant)]
+#[safety_constraint(true)]
+enum MyEnum {
+    A,
+    B(i32),
+}