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

Add vacuity test for contradictory requires clause #2793

Open
celinval opened this issue Sep 28, 2023 · 2 comments · May be fixed by #3623
Open

Add vacuity test for contradictory requires clause #2793

celinval opened this issue Sep 28, 2023 · 2 comments · May be fixed by #3623
Assignees
@carolynzech
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. Z-Contracts Issue related to code contracts
Milestone
Function Contracts

Comments

@celinval
Copy link
Contributor

Requested feature: Contract verification should fail if the requires clause can never be satisfied
Use case: Detect user mistakes when writing contracts
Link to relevant documentation (Rust reference, Nomicon, RFC):

Test case:

#[kani::requires(a > 5)]
#[kani::requires(a < 4)]
#[kani::ensures(result == a)]
fn buggy(a: u32) -> u32 {
    panic!("This code is never tested")
}

Without vacuity test, this contract verification will pass.
@celinval celinval added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label Sep 28, 2023
@celinval celinval added this to the Function Contracts MVP milestone Sep 28, 2023
@celinval
Copy link
Contributor Author

Thank you for the suggestion @camshaft

@JustusAdam
Copy link
Contributor

I'm impressed with how fast people are picking up contracts.

@feliperodri feliperodri self-assigned this Feb 28, 2024
@carolynzech carolynzech added the Z-Contracts Issue related to code contracts label Oct 21, 2024
@carolynzech carolynzech linked a pull request Oct 21, 2024 that will close this issue
Draft
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@carolynzech carolynzech

Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. Z-Contracts Issue related to code contracts
Projects
None yet
Milestone
Function Contracts
Development

Successfully merging a pull request may close this issue.

Fail verification if contract is vacuous carolynzech/kani
4 participants
@feliperodri @JustusAdam @celinval @carolynzech