Skip to content

Add autoharness to run-kani script and use in CI#334

Merged
tautschnig merged 30 commits intomodel-checking:mainfrom
tautschnig:autoharness-support
Apr 29, 2025
Merged

Add autoharness to run-kani script and use in CI#334
tautschnig merged 30 commits intomodel-checking:mainfrom
tautschnig:autoharness-support

Conversation

@tautschnig
Copy link
Member

@tautschnig tautschnig commented Apr 22, 2025 •
edited
Loading

Run a selected set of automatic harnesses where their previous, manual harnesses are being removed in this PR.

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

@tautschnig tautschnig self-assigned this Apr 22, 2025
@tautschnig tautschnig force-pushed the autoharness-support branch from 3c48d5a to 673fec8 Compare April 23, 2025 08:05
@tautschnig tautschnig force-pushed the autoharness-support branch from 673fec8 to a1bbbbb Compare April 23, 2025 11:11
@tautschnig tautschnig force-pushed the autoharness-support branch from 31bed92 to 267fa99 Compare April 24, 2025 08:55
@tautschnig tautschnig marked this pull request as ready for review April 24, 2025 12:20
@tautschnig tautschnig requested a review from a team as a code owner April 24, 2025 12:20
carolynzech
carolynzech reviewed Apr 24, 2025
View reviewed changes
@tautschnig tautschnig assigned carolynzech and unassigned tautschnig Apr 24, 2025
carolynzech
carolynzech approved these changes Apr 24, 2025
View reviewed changes
Copy link

@carolynzech carolynzech 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!

tautschnig added 14 commits April 25, 2025 20:37
@tautschnig
Use autoharness for num::<impl *>::wrapping_sh{l,r}
0c1b5c3
@tautschnig
Use autoharness for num::<impl *>::unchecked_sh{l,r}
2144ebe
@tautschnig
Use autoharness for num::<impl i*>::unchecked_neg
e7b0dc4
@tautschnig
Use autoharness for num::<impl *>::unchecked_{add,sub}
153f5d1
@tautschnig
Use autoharness for convert::num::<impl convert::From<num::nonzero::N…
bc70538 
…onZero<*>> for num::nonzero::NonZero<*>>::from
@tautschnig
Use autoharness for num::nonzero::NonZero::<*>::count_ones
a0daec5
@tautschnig
Use autoharness for num::nonzero::NonZero::<*>::rotate_{left,right}
f079d4c
@tautschnig
Use array for command_args to ensure quoting is retained
1e17495
@tautschnig
Do not try to use unset CBMC_PATCH variable
7798495
@tautschnig
Revert "Use autoharness for convert::num::<impl convert::From<num::no…
308f6a1 
…nzero::NonZero<*>> for num::nonzero::NonZero<*>>::from"

This reverts commit bc70538.
@tautschnig
Revert "Use autoharness for num::<impl *>::unchecked_{add,sub}"
a90ba68 
This reverts commit 153f5d1.
@tautschnig
Revert "Use autoharness for num::<impl i*>::unchecked_neg"
3aefe47 
This reverts commit e7b0dc4.
@tautschnig
Revert "Use autoharness for num::<impl *>::unchecked_sh{l,r}"
dcc1959 
This reverts commit 2144ebe.
@tautschnig
Revert "Use autoharness for num::<impl *>::wrapping_sh{l,r}"
7162c25 
This reverts commit 0c1b5c3.
@zjp-CN zjp-CN mentioned this pull request Apr 28, 2025
Open
qinheping
qinheping approved these changes Apr 28, 2025
View reviewed changes
@tautschnig tautschnig assigned tautschnig and unassigned qinheping Apr 29, 2025
tautschnig
tautschnig commented Apr 29, 2025
View reviewed changes
Copy link
Member Author

@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.

Re-run approvals.

@tautschnig tautschnig enabled auto-merge April 29, 2025 11:25
@tautschnig tautschnig added this pull request to the merge queue Apr 29, 2025
Merged via the queue into model-checking:main with commit f804a33 Apr 29, 2025
21 checks passed
@tautschnig tautschnig deleted the autoharness-support branch April 29, 2025 16:34
@tautschnig tautschnig mentioned this pull request Jun 26, 2025
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

2 more reviewers

@qinheping qinheping qinheping approved these changes

@carolynzech carolynzech carolynzech approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@tautschnig tautschnig

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@tautschnig @qinheping @carolynzech