Skip to content

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

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 30 commits into from
Apr 29, 2025
Merged

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

merged 30 commits into from
Apr 29, 2025
+133 −268

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
Squash duplicate space in markdown file
Loading
Loading status checks…
a1bbbbb
@tautschnig tautschnig force-pushed the autoharness-support branch from 673fec8 to a1bbbbb Compare April 23, 2025 11:11
@tautschnig
Use .0 instead of .as_usize
Loading
Loading status checks…
267fa99
@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
Make autoharness in run-kani.sh --run list optional
Loading
Loading status checks…
d4c6ec5
@tautschnig
Amend help
Loading
Loading status checks…
8064562
@tautschnig tautschnig assigned carolynzech and unassigned tautschnig Apr 24, 2025
@tautschnig
Fix help
Loading
Loading status checks…
96baf9d
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}
Loading
Loading status checks…
f079d4c
@tautschnig
Use array for command_args to ensure quoting is retained
Loading
Loading status checks…
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}"
Loading
Loading status checks…
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@qinheping qinheping

@carolynzech carolynzech

Assignees

@tautschnig tautschnig

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@tautschnig @qinheping @carolynzech