Skip to content

Run more automatic harnesses (use patterns w/ regex support) #397

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 3 commits into from
Jul 10, 2025
Merged

Run more automatic harnesses (use patterns w/ regex support) #397

merged 3 commits into from
Jul 10, 2025

Conversation

carolynzech
Copy link

@carolynzech carolynzech commented Jun 26, 2025 •
edited
Loading

Use the support for regexes added in model-checking/kani#4144 to run more automatic harnesses in CI. This brings us from 77 harnesses to 184.

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

@carolynzech carolynzech requested a review from a team as a code owner June 26, 2025 17:22
@carolynzech
Copy link
Author

carolynzech commented Jun 26, 2025 •
edited
Loading

@tautschnig Should we change the >::disjoint_bitor and >::unchecked_disjoint_bitor patterns, per the comment in this workflow file? I actually think we may as well just keep them to avoid doing <bool as ...>::disjoint_bitor, <i8 as ...>::disjoint_bitor, etc., but not sure if I'm missing something.
(At the very least we should remove the comment in the file about patterns not being supported before merging this).

@tautschnig
Copy link
Member

Thank you! Can we please also remove the manual harnesses for those? See my commits in #334 (those that I then also reverted in that PR).

@tautschnig
Copy link
Member

@tautschnig Should we change the >::disjoint_bitor and >::unchecked_disjoint_bitor patterns, per the comment in this workflow file? I actually think we may as well just keep them to avoid doing <bool as ...>::disjoint_bitor, <i8 as ...>::disjoint_bitor, etc., but not sure if I'm missing something. (At the very least we should remove the comment in the file about patterns not being supported before merging this).

Maybe we could make the patterns a bit more meaningful by doing something like <(.+)[[:space:]]as[[:space:]](.+)>::disjoint_bitor?

tautschnig
tautschnig requested changes Jul 3, 2025
View reviewed changes
Copy link
Member

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

Thank you for all this cleanup! Just a few lines that IMHO should be reinstated.

@tautschnig tautschnig added this pull request to the merge queue Jul 10, 2025
Merged via the queue into model-checking:main with commit a4edf5f Jul 10, 2025
25 checks passed
nilehmann pushed a commit to flux-rs/verify-rust-std that referenced this pull request Jul 16, 2025
@carolynzech @tautschnig @nilehmann
Run more automatic harnesses (use patterns w/ regex support) (model-c…
e8f8383 
…hecking#397)

Use the support for regexes added in
model-checking/kani#4144 to run more automatic
harnesses in CI. This brings us from 77 harnesses to 184.

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: Michael Tautschnig <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tautschnig tautschnig tautschnig approved these changes

@thanhnguyen-aws thanhnguyen-aws thanhnguyen-aws approved these changes

Assignees

@thanhnguyen-aws thanhnguyen-aws

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@carolynzech @tautschnig @thanhnguyen-aws