Replace deprecated proc-macro-error2 with proc-macro2-diagnostics

[tautschnig]

proc-macro-error2 is unmaintained (RUSTSEC-2026-0173). Migrate the kani_macros crate to proc-macro2-diagnostics, one of the alternatives recommended by the advisory.

The abort!/abort_call_site! macros (which panicked and were caught by the #[proc_macro_error] wrapper) are replaced by threading Result<TokenStream, Diagnostic> through the macro helpers and emitting the diagnostic at each entry point via Diagnostic::emit_as_item_tokens(). The structured note/help sub-diagnostics and spans are preserved, and proc-macro2-diagnostics auto-enables native nightly emission, so the compiler output is unchanged.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Pull request overview

This PR migrates the kani_macros proc-macro crate off the unmaintained proc-macro-error2 (flagged by RUSTSEC-2026-0173) to proc-macro2-diagnostics, reworking macro error handling to emit structured diagnostics without relying on panic-catching wrappers.

Changes:

• Replaced proc-macro-error2 usage (abort!, abort_call_site!, #[proc_macro_error]) with proc_macro2_diagnostics::Diagnostic-based error construction/emission.
• Refactored derive/proof macro helpers to return Result<_, Diagnostic> and emit diagnostics at macro entry points.
• Updated dependencies in Cargo.toml/Cargo.lock to remove proc-macro-error2 and add proc-macro2-diagnostics.

Reviewed changes

Copilot reviewed 5 out of 6 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
library/kani_macros/src/sysroot/loop_contracts/mod.rs	Replaces abort_call_site! with Diagnostic emission for unsupported loop forms.
library/kani_macros/src/lib.rs	Removes #[proc_macro_error] and migrates sysroot proof argument parsing to Diagnostic-based reporting.
library/kani_macros/src/derive.rs	Threads Result<_, Diagnostic> through derive helpers and emits diagnostics at entry points.
library/kani_macros/src/derive_bounded.rs	Converts union-derive failure to Diagnostic and emits at entry point.
library/kani_macros/Cargo.toml	Swaps proc-macro-error2 dependency for proc-macro2-diagnostics.
Cargo.lock	Updates lockfile entries to reflect dependency replacement.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.