Implement #[thrust::extern_spec_fn]

[coord-e]

No description provided.

[Copilot]

Pull request overview

This PR implements the #[thrust::extern_spec_fn] attribute, which enables developers to specify contracts for external functions by wrapping them with annotated specification functions. This allows applying Thrust's verification capabilities to standard library functions and other external code that cannot be directly annotated.

Key changes:

• Added new extern_spec_fn attribute path and detection mechanism
• Implemented DefId extraction to map specification functions to their target external functions
• Integrated extern_spec_fn functions into the trusted function set with proper type registration

Reviewed changes

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

Show a summary per file

File	Description
tests/ui/pass/extern_spec_take.rs	Passing test demonstrating correct usage of extern_spec_fn with std::mem::take
tests/ui/fail/extern_spec_take.rs	Failing test verifying that incorrect assertions are caught when using extern_spec_fn
src/analyze/annot.rs	Adds the extern_spec_fn_path() function to define the attribute path
src/analyze/local_def.rs	Implements detection and target DefId extraction for extern_spec_fn annotated functions
src/analyze/crate_.rs	Integrates extern_spec_fn into the analysis pipeline, treating them as trusted and registering their types

---

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