-
Notifications
You must be signed in to change notification settings - Fork 12.7k
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
classes with destructor should error if one tries an explicit copy #2823
Milestone
Comments
ghost
assigned catamorphism
Jul 7, 2012
This may become a non-issue when we stop using last-use to do optimization. I'm not completely sure. |
Postponing until #2633 is resolved. |
saethlin
pushed a commit
to saethlin/rust
that referenced
this issue
Apr 11, 2023
celinval
pushed a commit
to celinval/rust-dev
that referenced
this issue
Jun 4, 2024
…ust-lang#2809) This adds support for verifying the contracts of recursive functions inductively. The idea is quite simple. We use a global variable to track whether we're reentering a function and depending on that value we either continue with checking the contract or assume the hypothesis by using its replacement. The precise mechanism that I implemented is explained in the documentation [here](https://github.com/JustusAdam/kani/blob/a31176c79098205ca0b2c2b199cdf06653754551/library/kani_macros/src/sysroot/contracts.rs#L126) Resolves rust-lang#2724 **Open Question:** to facilitate induction the return type of the function must implement `kani::Arbitrary`. Since we can't discriminate between recursive and non-recursive functions in the proc-macro this means that this applies to all functions with contracts, not just recursive ones. This may be an unacceptable restriction. We could consider making inductive verification explicit with an annotation like `#[kani::inductive]` or conversely make inductive the default and let users opt-out with `#[kani::no_inductive]`. This is now tracked in rust-lang#2823 I had to remove the names of the functions in which the messages occur in the test cases, since they are now generated, hard to read names By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Zyad Hassan <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Even though the class has a destructor, it is valid rust code because it seems rust is ignoring the explicit copy because
let d = copy c
is the last use ofc
. I feel this is confusing, so I think rustc should report an error here.The text was updated successfully, but these errors were encountered: