Skip to content

Commit

Permalink
Fix format
Browse files Browse the repository at this point in the history
  • Loading branch information
adpaco-aws committed Jul 9, 2024
1 parent 7734715 commit 5aa04f5
Showing 1 changed file with 7 additions and 4 deletions.
11 changes: 7 additions & 4 deletions library/kani_macros/src/derive.rs
Original file line number Diff line number Diff line change
Expand Up @@ -426,15 +426,18 @@ fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream {
/// Generates an `Invariant` implementation where the `is_safe` function body is
/// the `attr` expression passed to the attribute macro.
/// Only available for structs.
pub fn attr_custom_invariant(attr: TokenStream, item: proc_macro::TokenStream) -> proc_macro::TokenStream {
pub fn attr_custom_invariant(
attr: TokenStream,
item: proc_macro::TokenStream,
) -> proc_macro::TokenStream {
let derive_item = parse_macro_input!(item as DeriveInput);
let item_name = &derive_item.ident;

if !matches!(derive_item.data, Data::Struct(..)) {
abort!(Span::call_site(), "Cannot define invariant for `{}`", item_name;
note = item_name.span() =>
"`#[kani::invariant(..)]` is only available for structs"
)
note = item_name.span() =>
"`#[kani::invariant(..)]` is only available for structs"
)
}

// Keep a copy of the original item to re-emit it later.
Expand Down

0 comments on commit 5aa04f5

Please sign in to comment.