Emit proc-macro expansion directly via quote! instead of delegating to __devirt_define!

crates/core/src/lib.rs

@@ -30,9 +30,12 @@
 //! generates:
 //! - `impl __XImpl for ConcreteType { ... }` with the `__spec_*` bodies
 //!
-//! Both the proc-macro attribute and the declarative macro delegate to
-//! `__devirt_define!`, a `#[doc(hidden)]` internal macro that contains
-//! all dispatch expansion logic.
+//! The proc-macro attribute (`#[devirt]`) emits the dispatch code
+//! directly via `quote!`, supporting the full range of method
+//! signatures that `syn` can parse (lifetimes, `unsafe fn`,
+//! supertraits, attributes, `extern "ABI" fn`, etc.).
+//! The declarative macro (`devirt!`) delegates to `__devirt_define!`,
+//! which has more limited syntax support.
 //!
 //! # Usage
 //!
@@ -121,6 +124,14 @@ extern crate kani;
 #[doc(hidden)]
 pub use paste::paste as __paste;
 
+/// Internal dispatch expansion macro.
+///
+/// This macro has **limited syntax support** compared to the
+/// `#[devirt]` proc-macro attribute. It only handles plain
+/// `fn method(&self, arg: Type) -> Ret;` signatures — no `unsafe fn`,
+/// method lifetimes, supertraits, method attributes, `where` clauses,
+/// or `extern "ABI" fn`. For the full feature set, use the proc-macro
+/// attribute (the default with the `macros` feature enabled).
 #[doc(hidden)]
 #[macro_export]
 macro_rules! __devirt_define {

crates/core/tests/equivalence.rs

@@ -95,6 +95,75 @@ fn decl_dispatch() {
     assert_eq!(c.val, 100);
 }
 
+// ── Extended proc-macro tests: supertraits, method lifetimes, #[must_use] ──
+
+#[cfg(feature = "macros")]
+mod attr_extended {
+    use core::fmt;
+
+    #[derive(Debug)]
+    pub struct ExtHot {
+        pub val: u64,
+        pub label: String,
+    }
+
+    #[derive(Debug)]
+    pub struct ExtCold {
+        pub val: u64,
+        pub label: String,
+    }
+
+    #[devirt::devirt(ExtHot)]
+    pub trait Inspectable: fmt::Debug {
+        #[must_use]
+        fn value(&self) -> u64;
+        // Explicit lifetime to exercise method-lifetime support.
+        fn name<'a>(&'a self) -> &'a str;
+        fn set_val(&mut self, v: u64);
+    }
+
+    #[devirt::devirt]
+    impl Inspectable for ExtHot {
+        fn value(&self) -> u64 { self.val }
+        fn name(&self) -> &str { &self.label }
+        fn set_val(&mut self, v: u64) { self.val = v; }
+    }
+
+    #[devirt::devirt]
+    impl Inspectable for ExtCold {
+        fn value(&self) -> u64 { self.val + 1 }
+        fn name(&self) -> &str { &self.label }
+        fn set_val(&mut self, v: u64) { self.val = v + 1; }
+    }
+}
+
+#[cfg(feature = "macros")]
+#[test]
+fn attr_extended_dispatch() {
+    use attr_extended::{ExtCold, ExtHot, Inspectable};
+
+    // Supertraits: dyn Inspectable implements Debug
+    let h = ExtHot { val: 42, label: "hot".into() };
+    let c = ExtCold { val: 42, label: "cold".into() };
+    drop(format!("{:?}", &h as &dyn Inspectable));
+
+    // #[must_use] + non-void &self
+    assert_eq!((&h as &dyn Inspectable).value(), 42);
+    assert_eq!((&c as &dyn Inspectable).value(), 43);
+
+    // Method lifetimes
+    assert_eq!((&h as &dyn Inspectable).name(), "hot");
+    assert_eq!((&c as &dyn Inspectable).name(), "cold");
+
+    // &mut self
+    let mut h = ExtHot { val: 0, label: "hot".into() };
+    let mut c = ExtCold { val: 0, label: "cold".into() };
+    (&mut h as &mut dyn Inspectable).set_val(10);
+    (&mut c as &mut dyn Inspectable).set_val(10);
+    assert_eq!(h.val, 10);
+    assert_eq!(c.val, 11);
+}
+
 #[cfg(feature = "macros")]
 #[test]
 fn attr_dispatch() {

crates/core/tests/ui_attr.rs

@@ -8,7 +8,12 @@ fn ui_attr() {
     t.pass("tests/ui_attr/attr_all_arms.rs");
     t.pass("tests/ui_attr/attr_unsafe_trait.rs");
     t.pass("tests/ui_attr/attr_method_attrs.rs");
+    t.pass("tests/ui_attr/attr_unsafe_fn.rs");
+    t.pass("tests/ui_attr/attr_method_lifetimes.rs");
+    t.pass("tests/ui_attr/attr_supertraits.rs");
+    t.pass("tests/ui_attr/attr_must_use.rs");
     t.compile_fail("tests/ui_attr/attr_missing_args.rs");
+    t.compile_fail("tests/ui_attr/attr_unsafe_missing_on_impl.rs");
     t.compile_fail("tests/ui_attr/attr_args_on_impl.rs");
     t.compile_fail("tests/ui_attr/attr_on_struct.rs");
 }

crates/core/tests/ui_attr/attr_method_lifetimes.rs

@@ -0,0 +1,33 @@
+struct Hot {
+    name: String,
+}
+
+struct Cold {
+    name: String,
+}
+
+#[devirt::devirt(Hot)]
+pub trait Named {
+    fn name<'a>(&'a self) -> &'a str;
+}
+
+#[devirt::devirt]
+impl Named for Hot {
+    fn name<'a>(&'a self) -> &'a str { &self.name }
+}
+
+#[devirt::devirt]
+impl Named for Cold {
+    fn name<'a>(&'a self) -> &'a str { &self.name }
+}
+
+fn greet(n: &dyn Named) -> String {
+    format!("Hello, {}!", n.name())
+}
+
+fn main() {
+    let h = Hot { name: "world".into() };
+    let c = Cold { name: "rust".into() };
+    assert_eq!(greet(&h), "Hello, world!");
+    assert_eq!(greet(&c), "Hello, rust!");
+}

crates/core/tests/ui_attr/attr_must_use.rs

@@ -0,0 +1,32 @@
+struct Hot {
+    val: f64,
+}
+
+struct Cold {
+    val: f64,
+}
+
+#[devirt::devirt(Hot)]
+pub trait Computed {
+    #[must_use]
+    fn compute(&self) -> f64;
+}
+
+#[devirt::devirt]
+impl Computed for Hot {
+    fn compute(&self) -> f64 { self.val * 2.0 }
+}
+
+#[devirt::devirt]
+impl Computed for Cold {
+    fn compute(&self) -> f64 { self.val * 3.0 }
+}
+
+fn main() {
+    let h = Hot { val: 1.0 };
+    let c = Cold { val: 1.0 };
+    let dh: &dyn Computed = &h;
+    let dc: &dyn Computed = &c;
+    let _ = dh.compute(); // should NOT warn (result is used via let _)
+    let _ = dc.compute();
+}

crates/core/tests/ui_attr/attr_supertraits.rs

@@ -0,0 +1,39 @@
+use std::fmt::Debug;
+
+#[derive(Debug)]
+struct Hot {
+    val: u64,
+}
+
+#[derive(Debug)]
+struct Cold {
+    val: u64,
+}
+
+#[devirt::devirt(Hot)]
+pub trait Inspectable: Debug {
+    fn value(&self) -> u64;
+}
+
+#[devirt::devirt]
+impl Inspectable for Hot {
+    fn value(&self) -> u64 { self.val }
+}
+
+#[devirt::devirt]
+impl Inspectable for Cold {
+    fn value(&self) -> u64 { self.val + 1 }
+}
+
+fn inspect(i: &dyn Inspectable) -> String {
+    format!("{:?} = {}", i, i.value())
+}
+
+fn main() {
+    let h = Hot { val: 42 };
+    let c = Cold { val: 42 };
+    let s = inspect(&h);
+    assert!(s.contains("42"), "expected '42' in '{s}'");
+    let s = inspect(&c);
+    assert!(s.contains("43"), "expected '43' in '{s}'");
+}

crates/core/tests/ui_attr/attr_unsafe_fn.rs

@@ -0,0 +1,32 @@
+struct Hot {
+    data: *const u8,
+}
+
+struct Cold {
+    data: *const u8,
+}
+
+#[devirt::devirt(Hot)]
+pub trait Dangerous {
+    unsafe fn deref(&self) -> u8;
+}
+
+#[devirt::devirt]
+impl Dangerous for Hot {
+    unsafe fn deref(&self) -> u8 { unsafe { *self.data } }
+}
+
+#[devirt::devirt]
+impl Dangerous for Cold {
+    unsafe fn deref(&self) -> u8 { unsafe { *self.data } }
+}
+
+fn main() {
+    let val: u8 = 42;
+    let h = Hot { data: &val };
+    let c = Cold { data: &val };
+    let dh: &dyn Dangerous = &h;
+    let dc: &dyn Dangerous = &c;
+    assert_eq!(unsafe { dh.deref() }, 42);
+    assert_eq!(unsafe { dc.deref() }, 42);
+}

crates/core/tests/ui_attr/attr_unsafe_missing_on_impl.rs

@@ -0,0 +1,16 @@
+struct Hot {
+    val: u64,
+}
+
+#[devirt::devirt(Hot)]
+pub unsafe trait Trusted {
+    fn verify(&self) -> bool;
+}
+
+// Missing `unsafe` on impl — should fail because __TrustedImpl is unsafe.
+#[devirt::devirt]
+impl Trusted for Hot {
+    fn verify(&self) -> bool { self.val > 0 }
+}
+
+fn main() {}

crates/core/tests/ui_attr/attr_unsafe_missing_on_impl.stderr

@@ -0,0 +1,12 @@
+error[E0200]: the trait `__TrustedImpl` requires an `unsafe impl` declaration
+  --> tests/ui_attr/attr_unsafe_missing_on_impl.rs:11:1
+   |
+11 | #[devirt::devirt]
+   | ^^^^^^^^^^^^^^^^^
+   |
+   = note: the trait `__TrustedImpl` enforces invariants that the compiler can't check. Review the trait documentation and make sure this implementation upholds those invariants before adding the `unsafe` keyword
+   = note: this error originates in the attribute macro `devirt::devirt` (in Nightly builds, run with -Z macro-backtrace for more info)
+help: add `unsafe` to this trait implementation
+   |
+11 | unsafe #[devirt::devirt]
+   | ++++++