can't get the span of an arbitrary parsed attribute

[zjp-CN]

thread 'standard_proof' panicked at tests/snapshots.rs:11:5:
Failed to test standard_proof.rs:
The application panicked (crashed).
Message:  can't get the span of an arbitrary parsed attribute: Parsed(Stability { stability: Stability { level: Unstable { reason: None, issue
: Some(81513), is_soft: false, implied_by: None }, feature: "ptr_metadata" }, span: /home/zjp/.rustup/toolchains/nightly-2025-04-01-x86_64-unk
nown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/metadata.rs:110:1: 110:55 (#0) })
Location: /home/zjp/.rustup/toolchains/nightly-2025-04-01-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/rustc_hir/src/hir.rs:1204

Seems that it's problematic to query span of some attributes?

#[unstable(feature = "ptr_metadata", issue = "81513")] // 💥fails to get this attr
#[inline]
pub const fn from_raw_parts<T: ?Sized>(
    data_pointer: *const impl Thin,
    metadata: <T as Pointee>::Metadata,
) -> *const T {
    aggregate_raw_ptr(data_pointer, metadata)
}

panic location: https://github.com/rust-lang/rust/blob/71b68da1bd9fa6afb9f964a731e9c843ab0862bd/compiler/rustc_hir/src/hir.rs#L1204

    fn span(&self) -> Span {
        match &self {
            Attribute::Unparsed(u) => u.span,
            // FIXME: should not be needed anymore when all attrs are parsed
            Attribute::Parsed(AttributeKind::Deprecation { span, .. }) => *span,
            Attribute::Parsed(AttributeKind::DocComment { span, .. }) => *span,
            a => panic!("can't get the span of an arbitrary parsed attribute: {a:?}"),
        }
    }

So the problem is some internal attrs don't contain span, and attr.span() is infallible.

The solution is to extract some kinds of attrs, but most attrs on fns are not useful, except contracts.
The contracts come from two flavours: builtin-Rust, or custom tools

• builtin-Rust contracts seems not a kind of attr, it may be converted to some generated code into the function, thus skip this case
• #[kanitool::contract] is important, because once the contract content changes, proofs related to this contracts need to rerun