Skip to content

Add harnesses for all functions in Alignment - #42

Merged
tautschnig merged 15 commits into
model-checking:mainfrom
tautschnig:align-harness
Aug 20, 2024
Merged

Add harnesses for all functions in Alignment#42
tautschnig merged 15 commits into
model-checking:mainfrom
tautschnig:align-harness

Conversation

@tautschnig

@tautschnigtautschnig commented Jul 23, 2024

Copy link
Copy Markdown
Member

In #33 a contract was added to Alignment::new_unchecked, but its verification was only implicit through Layout, and may be affected by future changes to the contract that was added to Layout. This commit remedies this by adding a separate harness just for Alignment.

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

@tautschnig
Add harness for Alignment::new_unchecked
44824f1
In model-checking#33 a contract was added to `Alignment::new_unchecked`, but its
verification was only implicit through `Layout`, and may be affected by
future changes to the contract that was added to `Layout`. This commit
remedies this by adding a separate harness just for `Alignment`.
@tautschnig
tautschnig requested a review from a team as a code ownerJuly 23, 2024 10:51
@tautschnigtautschnig mentioned this pull request Jul 23, 2024
Merged
celinval
celinval reviewed Jul 23, 2024
View reviewed changes
Comment threadlibrary/core/src/ptr/alignment.rs Outdated
@tautschnigtautschnig changed the title Add harness for Alignment::new_uncheckedAdd harnesses for all functions in AlignmentJul 24, 2024
celinval
celinval reviewed Jul 29, 2024
View reviewed changes

@celinvalcelinval left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me. Thanks

Comment threadlibrary/core/src/ptr/alignment.rs
@feliperodri
feliperodri self-requested a review July 30, 2024 19:10
feliperodri
feliperodri requested changes Jul 30, 2024
View reviewed changes
Comment threadlibrary/core/src/ptr/alignment.rs
Comment threadlibrary/core/src/ptr/alignment.rs
Comment threadlibrary/core/src/ptr/alignment.rs Outdated
Comment threadlibrary/core/src/ptr/alignment.rs Outdated
@feliperodrifeliperodri mentioned this pull request Jul 30, 2024
Merged
feliperodri
feliperodri approved these changes Aug 13, 2024
View reviewed changes

@feliperodrifeliperodri left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, but did you try the safety_constraint?

@tautschnig

tautschnig commented Aug 14, 2024

Copy link
Copy Markdown
MemberAuthor

LGTM, but did you try the safety_constraint?

No, because I can't get Arbitrary to work in the first place, see #42 (comment). Perhaps all this will work when upgrading Kani?

@celinval

celinval commented Aug 14, 2024

Copy link
Copy Markdown

LGTM, but did you try the safety_constraint?

No, because I can't get Arbitrary to work in the first place, see #42 (comment). Perhaps all this will work when upgrading Kani?

Please see my reply above

@celinval

celinval commented Aug 17, 2024

Copy link
Copy Markdown

Why did you revert the impl Arbitrary? Isn't that what we want (except for the transmute call).

@tautschnig

tautschnig commented Aug 17, 2024

Copy link
Copy Markdown
MemberAuthor

Why did you revert the impl Arbitrary? Isn't that what we want (except for the transmute call).

I thought it was causing the compile errors, but then I realised it’s #49 that’s needed. Will continue on this once Kani and this repo are back in a working state.

@tautschnig

tautschnig commented Aug 20, 2024

Copy link
Copy Markdown
MemberAuthor

Why did you revert the impl Arbitrary? Isn't that what we want (except for the transmute call).

I thought it was causing the compile errors, but then I realised it’s #49 that’s needed. Will continue on this once Kani and this repo are back in a working state.

Now successfully using Arbitrary.

@tautschnig
tautschnig merged commit 03c735b into model-checking:mainAug 20, 2024
@tautschnig
tautschnig deleted the align-harness branch August 20, 2024 12:25
szlee118 pushed a commit to stogaru/verify-rust-std that referenced this pull request Oct 17, 2024
@tautschnig
Add harnesses for all functions in Alignment (model-checking#42)
c04de3d
btj pushed a commit to btj/verify-rust-std that referenced this pull request Aug 22, 2025
@Zalathar
Rollup merge ofrust-lang#145051- bjorn3:prevent_linkage_symbol_name…
432a4f2
…_collision, r=petrochenkov
Prevent name collisions with internal implementation details
The implementation of the linkage attribute inside extern blocks defines symbols starting with _rust_extern_with_linkage_. If someone tries to also define this symbol you will get a symbol conflict or even an ICE. By adding an unpredictable component to the symbol name, this becomes less of an issue.
Spawned from the discussion at [#t-compiler > About static variables &model-checking#96;_rust_extern_with_linkage_&model-checking#42;&model-checking#96;](https://rust-lang.zulipchat.com/#narrow/channel/131828-t-compiler/topic/About.20static.20variables.20.60_rust_extern_with_linkage_*.60) cc `@ywxt`
Fixesrust-lang#144940
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@feliperodrifeliperodrifeliperodri approved these changes
+2 more reviewers
@celinvalcelinvalcelinval left review comments
@zhassan-awszhassan-awszhassan-aws left review comments
Reviewers whose approvals may not affect merge requirements

Assignees

@feliperodrifeliperodri

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@tautschnig@celinval@feliperodri@zhassan-aws