Add unsafe callee detection for verification targets.#239
Merged
Conversation
…lees Extend verify scan to collect unsafe callees
hxuhack
added a commit
that referenced
this pull request
May 12, 2026
* Add a new cli option for verification. (#237) * add verify test * feat: add verify command with --scan option * fix compilation errors * fix bugs * refactor verification module to make pipeline clearer (#238) * Add unsafe callee detection for verification targets. (#239) * Extend verify scan to collect unsafe callees * add unsafe callees * * rename scan to collect * add std contracts * add 2 test cases for alignment verification (#240) * extract callee contracts. --------- * Update verify target collector (#242) * add local verify contract module * add local verify helper module * fix verify local module paths and type inference * add English documentation to verify collect module * update * refactor verify (#243) * add struct invariants (#244) * add a struct example * Refactor verify targets into function and struct targets * Support struct field and generic resolution in verify helpers * Simplify verify target collector structure * Fix struct invariant collection for local struct targets * Read struct invariants from local struct HIR items * fix compilation bug * fix bug * Add RAPx attribute parser under verify * Use shared RAPx attribute parser in verify target analysis * Fix RAPx attribute parsing with syn outer attributes * Use method context when parsing struct invariants * update rapx attribute parsing (#245) * merge two get fn proterty functions * delete walk_fn * refactor: simplify RAPx attribute parser flow * refactor: deduplicate RAPx verify attribute collection * refactor: remove requires kind filtering * Associate RAPx kind with preceding property * update attribute parser (#246) * docs: add doc comments and inline comments to attr_parser.rs * docs: clarify requires attribute parser comments and naming * Refactor RAPx requires attribute parsing for semicolon metadata * Simplify RAPx requires attribute parser for single property syntax * Refactor src modules into analysis, check, and verify namespaces with dedicated CLI check args * Complete physical `analysis` → `check`/`verify` module migration in `rapx` (#247) --------- Co-authored-by: ClearLove <98693523+DiuDiu777@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.