Emit annotated item in error message #3495
Description
The replacement of the unmaintained proc-macro-error crate with the proc-macro-error2 crate in #3493 resulted in a diff in the error message Kani emits for https://github.com/model-checking/kani/tree/main/tests/ui/derive-arbitrary/union.
With proc-macro-error, the error was:
error: Cannot derive `Arbitrary` for `Wrapper` union
--> union.rs:5:10
|
5 | #[derive(kani::Arbitrary)]
| ^^^^^^^^^^^^^^^
|
note: `#[derive(Arbitrary)]` cannot be used for unions such as `Wrapper`
--> union.rs:6:7
|
6 | union Wrapper {
| ^^^^^^^
= note: this error originates in the derive macro `kani::Arbitrary` (in Nightly builds, run with -Z macro-backtrace for more info)
With proc-macro-error2, the error is:
error: Cannot derive `Arbitrary` for `Wrapper` union
= note: `#[derive(Arbitrary)]` cannot be used for unions such as `Wrapper`
--> union.rs:5:10
|
5 | #[derive(kani::Arbitrary)]
| ^^^^^^^^^^^^^^^
|
= note: this error originates in the derive macro `kani::Arbitrary` (in Nightly builds, run with -Z macro-backtrace for more info)
The two notable differences are:
- The annotated item (
union Wrapper) is no longer included in the error - The first
notedoes not appear after the span.
We should investigate if it's possible to restore the previous behavior.