diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index a581f79790be..ae3701f66234 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -274,7 +274,7 @@ fn parse_safety_expr(ident: &Ident, field: &syn::Field) -> Option { } } -fn parse_safety_expr_struct(ident: &Ident, derive_input: &DeriveInput) -> Option { +fn parse_safety_expr_input(ident: &Ident, derive_input: &DeriveInput) -> Option { let name = ident; let mut safety_attr = None; @@ -407,8 +407,9 @@ fn safety_conds_opt( derive_input: &DeriveInput, trait_name: &str, ) -> Option { - 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()]` attached to struct diff --git a/tests/ui/attr-invariant/double-attr-invariant/double-attr-invariant.rs b/tests/ui/safety-constraint-attribute/double-attribute/double-attribute.rs similarity index 100% rename from tests/ui/attr-invariant/double-attr-invariant/double-attr-invariant.rs rename to tests/ui/safety-constraint-attribute/double-attribute/double-attribute.rs diff --git a/tests/ui/attr-invariant/double-attr-invariant/expected b/tests/ui/safety-constraint-attribute/double-attribute/expected similarity index 100% rename from tests/ui/attr-invariant/double-attr-invariant/expected rename to tests/ui/safety-constraint-attribute/double-attribute/expected diff --git a/tests/ui/attr-invariant/invalid-pred-error/expected b/tests/ui/safety-constraint-attribute/invalid-pred-error/expected similarity index 100% rename from tests/ui/attr-invariant/invalid-pred-error/expected rename to tests/ui/safety-constraint-attribute/invalid-pred-error/expected diff --git a/tests/ui/attr-invariant/invalid-pred-error/invalid-pred-error.rs b/tests/ui/safety-constraint-attribute/invalid-pred-error/invalid-pred-error.rs similarity index 83% rename from tests/ui/attr-invariant/invalid-pred-error/invalid-pred-error.rs rename to tests/ui/safety-constraint-attribute/invalid-pred-error/invalid-pred-error.rs index 6ba424fad2e7..89c862bb50c3 100644 --- a/tests/ui/attr-invariant/invalid-pred-error/invalid-pred-error.rs +++ b/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; diff --git a/tests/ui/safety-constraint-attribute/no-struct-error/expected b/tests/ui/safety-constraint-attribute/no-struct-error/expected new file mode 100644 index 000000000000..fe258440adfb --- /dev/null +++ b/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 \ No newline at end of file diff --git a/tests/ui/safety-constraint-attribute/no-struct-error/no-struct-error.rs b/tests/ui/safety-constraint-attribute/no-struct-error/no-struct-error.rs new file mode 100644 index 000000000000..092bbe1319c7 --- /dev/null +++ b/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), +}