Skip to content

dyn Trait proof for contracts of byte_offset_from - #196

Merged
tautschnig merged 17 commits into
model-checking:mainfrom
stogaru:verify/ptr_byte_offset_from_dyn
Dec 10, 2024
Merged

tautschnig merged 17 commits into
model-checking:mainfrom
stogaru:verify/ptr_byte_offset_from_dyn

Conversation

@stogaru

@stogaru stogaru commented Nov 29, 2024 •

Copy link
Copy Markdown

Towards #76

This pull request implements proof for contracts for byte_offset_from verifying dyn Trait pointee types. Both const and mut versions are included.

It serves as an addition to an existing #186 but is submitted separately to avoid disrupting the ongoing review process for that PR. This PR should only be merged after the other PR has been merged.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

PoC: @xsxszab

@stogaru
stogaru requested a review from a team as a code owner November 29, 2024 03:07
@stogaru stogaru changed the title Verify/ptr byte offset from dyn dyn Trait proof for contracts of byte_offset_from Nov 29, 2024
@stogaru
stogaru marked this pull request as draft November 29, 2024 04:51
@stogaru
stogaru marked this pull request as ready for review December 9, 2024 21:01
@stogaru stogaru removed their assignment Dec 9, 2024
@feliperodri

Copy link
Copy Markdown
Member

@stogaru could you resolve the merge conflicts?

Comment thread library/core/src/ptr/const_ptr.rs Outdated
Comment thread library/core/src/ptr/mut_ptr.rs Outdated
@tautschnig
tautschnig enabled auto-merge (squash) December 10, 2024 10:12
@tautschnig
tautschnig merged commit 82893c5 into model-checking:main Dec 10, 2024
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.

4 participants