Skip to content

Commit

Permalink
Fix format
Browse files Browse the repository at this point in the history
  • Loading branch information
adpaco-aws committed Jun 17, 2024
1 parent 82a194b commit 0bc5b1b
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 @@ -259,15 +259,18 @@ fn struct_safe_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 0bc5b1b

Please sign in to comment.