Skip to content

Add proof harnesses for unchecked_disjoint_bitor on unsigned integer … - #662

Draft
Tianshu-Huang wants to merge 2 commits into
model-checking:mainfrom
Tianshu-Huang:add-unchecked-disjoint-bitor-harness
Draft

Add proof harnesses for unchecked_disjoint_bitor on unsigned integer …#662
Tianshu-Huang wants to merge 2 commits into
model-checking:mainfrom
Tianshu-Huang:add-unchecked-disjoint-bitor-harness

Conversation

@Tianshu-Huang

Copy link
Copy Markdown

Summary

  • Add 6 proof_for_contract harnesses for unchecked_disjoint_bitor on u8, u16, u32, u64, u128, and usize
  • These functions had contracts (#[requires((self & other) == 0)]) but no verification harnesses

Verification

  • All 6 harnesses pass locally with : ./scripts/run-kani.sh --kani-args --harness checked_unchecked_disjoint_bitor --output-format terse
  • Complete - 6 successfully verified harnesses, 0 failures, 6 total.

@Tianshu-Huang
Tianshu-Huang requested a review from a team as a code owner August 27, 2026 23:31
@Tianshu-Huang
Tianshu-Huang marked this pull request as draft August 27, 2026 23:51
@Tianshu-Huang
Tianshu-Huang force-pushed the add-unchecked-disjoint-bitor-harness branch from bba126d to fdd4bb5 Compare August 28, 2026 00:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant