Skip to content
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

Option that causes verification to fail for uncoverable cover statements #2299

Open
adpaco-aws opened this issue Mar 13, 2023 · 1 comment
Open

Option that causes verification to fail for uncoverable cover statements #2299

adpaco-aws opened this issue Mar 13, 2023 · 1 comment
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one. T-User Tag user issues / requests

Comments

@adpaco-aws
Copy link
Contributor

The RFC for cover statements mentioned:

We can consider adding an option that would cause verification to fail if a cover property was unsatisfiable or unreachable, e.g. --fail-uncoverable.

We are now aware that some users want this option.

It'd be great if we could include this option as part of the "more granular expectations" discussed here. Let's say we had a language to describe expectations for regular properties and cover statements. Then, this expectation is essentially that all cover statements are satisfied.
@adpaco-aws adpaco-aws added [C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one. T-User Tag user issues / requests labels Mar 13, 2023
@adpaco-aws adpaco-aws self-assigned this Mar 13, 2023
@adpaco-aws
Copy link
Contributor Author

We've agreed on supplying the option as it was described in the RFC. In other words, we don't need to include as part of the "more granular expectations" work since it's unknown whether they would be useful or not.

The main problem with this option is how it interacts with #[kani::should_panic] and other attributes. There isn't a conflict per se (verification will be successful if both verification panics AND cover statements are covered), but I'm afraid that adding more options that modify the verification result complicates post-processing too much.

@adpaco-aws adpaco-aws moved this to Todo in Kani 2023-06-19 Jun 5, 2023
@adpaco-aws adpaco-aws moved this from Todo to In Progress in Kani 2023-06-19 Jun 5, 2023
This was referenced Jun 12, 2023
Merged
Open
Closed
@adpaco-aws adpaco-aws mentioned this issue Jan 3, 2024
Merged
adpaco-aws added a commit that referenced this issue Jan 12, 2024
@adpaco-aws
Rethink should_panic and fail_uncoverable options as global condi…
fd12a28 
…tions (#2967)

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] User Experience An UX enhancement for an existing feature. Including deprecation of an existing one. T-User Tag user issues / requests
Projects
No open projects
Kani 2023-06-19
Status: In Progress
Milestone
No milestone
1 participant
@adpaco-aws