Skip to content

Cannot use multiple #[stub_verified(..)] attributes to a single harness #3804

@ShoyuVanilla

Description

@ShoyuVanilla

The docs says

/// You may use multiple `stub_verified` attributes on a single harness.
///
/// This is part of the function contract API, for more general information see
/// the [module-level documentation](../kani/contracts/index.html).
#[proc_macro_attribute]
pub fn stub_verified(attr: TokenStream, item: TokenStream) -> TokenStream {
attr_impl::stub_verified(attr, item)
}

but actually, we can't because

KaniAttributeKind::StubVerified => {
expect_single(self.tcx, kind, &attrs);
}

I'd like to fix this but I wonder which way it was originally intended for.

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] BugThis is a bug. Something isn't working.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions