refactor analysis check verify#248
Merged
Merged
Conversation
* add verify test * feat: add verify command with --scan option * fix compilation errors * fix bugs
* Extend verify scan to collect unsafe callees * add unsafe callees
* add std contracts * add 2 test cases for alignment verification (#240) * extract callee contracts. ---------
* 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
* 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
* 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
* 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
… dedicated CLI check args
…rapx` (#247) authored-by: hxuhack <13302178+hxuhack@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
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.