This pull request addresses several issues across the Sanctifier contracts and tooling by introducing formal verification assertions, integration tests, and fixing formatting.
- Formal Verification (Reentrancy Guard): Added explicit invariants to
contracts/reentrancy-guard/src/lib.rsthat the Z3 solver backend can analyze. - Integration Tests (Main Tooling): Added integration tests for
tooling/sanctifier-cli/src/main.rs, testing the CLI against mock workspaces. - Integration Tests (Configuration): Added integration tests for configuration processing (mocking
tooling/sanctifier-cli/src/config.rs) to ensure SARIF/JSON outputs accurately reflect custom workspaces. - Documentation Formatting: Restructured
README.mdto use better Markdown formatting, including tables and callouts. - Vulnerable Contract Syntax: Fixed a missing delimiter in
contracts/vulnerable-contract/src/lib.rswhich was breakingcargo fmt.
Closes #1401 Closes #1402 Closes #1403 Closes #1406