-
Notifications
You must be signed in to change notification settings - Fork 91
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.
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
Rethink should_panic
and fail_uncoverable
options as global conditions
#2967
Rethink should_panic
and fail_uncoverable
options as global conditions
#2967
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good. How will this interact with the cover_or_fail
macro proposed in #2792?
Thank you! Good question. First of all, the interaction would depend on how the macro is implemented. I'm not aware of any specific proposal to do that, but I'm happy to discuss it considering the two options I've thought about. So please take what follows with a grain of salt because I may not be considering all options/cases. The first option is to implement Another option is to have Also, I wanted to point out that, assuming |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sounds good.
These are the auto-generated release notes for comparison purposes: ## What's Changed * Rethink `should_panic` and `fail_uncoverable` options as global conditions by @adpaco-aws in #2967 * Upgrade toolchain to nightly-2024-01-17 by @celinval in #2976 * Benchcomp visualize: fix missing import by @tautschnig in #2977 * Cargo update 2024-01-18 by @remi-delmas-3000 in #2978 **Full Changelog**: kani-0.44.0...kani-0.45.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
These are the auto-generated release notes for comparison purposes: ## What's Changed * Rethink `should_panic` and `fail_uncoverable` options as global conditions by @adpaco-aws in model-checking#2967 * Upgrade toolchain to nightly-2024-01-17 by @celinval in model-checking#2976 * Benchcomp visualize: fix missing import by @tautschnig in model-checking#2977 * Cargo update 2024-01-18 by @remi-delmas-3000 in model-checking#2978 **Full Changelog**: model-checking/kani@kani-0.44.0...kani-0.45.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This PR is the next step to rework/introduce the
should_panic
/fail_uncoverable
options as global conditions.Until now, we haven't had a concrete proposal to do so other than the implementation in #2532. This PR presents one for each option in their respective RFCs. I'd like to agree on this design before starting the code review for #2532.
Related to #1905 #2272 #2299 #2516
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.