Skip to content

Add harnesses for all public functions of Layout - #43

Merged
carolynzech merged 23 commits into
model-checking:mainfrom
tautschnig:layout-harnesses
Oct 2, 2024
Merged

Add harnesses for all public functions of Layout#43
carolynzech merged 23 commits into
model-checking:mainfrom
tautschnig:layout-harnesses

Conversation

@tautschnig

@tautschnigtautschnig commented Jul 23, 2024

Copy link
Copy Markdown
Member

Exercise all public member functions of Layout and assert properties over the result. Some of those should, perhaps, become ensures clauses.

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 harnesses for all public functions of Layout
96f1603
Exercise all public member functions of `Layout` and assert properties
over the result. Some of those should, perhaps, become `ensures`
clauses.
@tautschnig
tautschnig requested a review from a team as a code ownerJuly 23, 2024 12:42
celinval
celinval reviewed Jul 30, 2024
View reviewed changes
Comment threadlibrary/core/src/alloc/layout.rs
Comment threadlibrary/core/src/alloc/layout.rs Outdated
Comment threadlibrary/core/src/alloc/layout.rs Outdated
@feliperodri
feliperodri self-requested a review July 30, 2024 19:09
feliperodri
feliperodri reviewed Jul 30, 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.

Some comments from #42 also apply here. So I think maybe we should merge that previous PR first and implement some of the cleanups requested there in this one (e.g., using kani::Arbitrary and moving assertions to ensures clauses).

celinval
celinval reviewed Aug 20, 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.

I haven't finished yet

Comment threadlibrary/core/src/alloc/layout.rs Outdated
Comment threadlibrary/core/src/alloc/layout.rs
Comment threadlibrary/core/src/alloc/layout.rs
Comment threadlibrary/core/src/alloc/layout.rs Outdated
Comment threadlibrary/core/src/alloc/layout.rs Outdated
@rahulku

rahulku commented Sep 13, 2024

Copy link
Copy Markdown

is this blocked on something?

celinval
celinval approved these changes Oct 2, 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.

Sorry, I was hoping the other stuff would be in by now. So let's unblock this PR and we can go back and improve this once the Invariant PR merges.

@carolynzech
carolynzech enabled auto-merge (squash) October 2, 2024 21:20
@carolynzech
carolynzech merged commit 024d84b into model-checking:mainOct 2, 2024
@tautschnig
tautschnig deleted the layout-harnesses branch October 8, 2024 09:16
szlee118 pushed a commit to stogaru/verify-rust-std that referenced this pull request Oct 17, 2024
@tautschnig@celinval
Add harnesses for all public functions ofLayout(model-checking#43)
bbffae9
Exercise all public member functions of `Layout` and assert properties
over the result. Some of those should, perhaps, become `ensures`
clauses.
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---------
Co-authored-by: Celina G. Val <celinval@amazon.com>
@celinvalcelinval mentioned this pull request Oct 17, 2024
Merged
hxuhack pushed a commit to safer-rust/rapx-verify-rust-std that referenced this pull request Sep 23, 2025
@zjp-CN
Merge pull requestmodel-checking#43from os-checker/safety-parser_st…
1a4c511
…ring_literal_quote
Fix: don't emit string literal quotes and add extra 2 newlines for each SP doc item
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

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

Assignees

@celinvalcelinval

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@tautschnig@rahulku@feliperodri@celinval@carolynzech