Skip to content

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

Merged
tautschnig merged 3 commits intomodel-checking:mainfrom
carolynzech:autoharness-regex
Jul 10, 2025
Merged

Run more automatic harnesses (use patterns w/ regex support)#397
tautschnig merged 3 commits intomodel-checking:mainfrom
carolynzech:autoharness-regex

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

tautschnig commented Jun 26, 2025

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 commented Jun 26, 2025

@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
@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 <tautschn@amazon.com>
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