-
Notifications
You must be signed in to change notification settings - Fork 13.3k
LLVM failure compiling borrow #3026
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
Comments
Still crashes if I eliminate the "implicit copy" warning, by replacing x in the arg list with
or
(is there a better way to silence the warning?)
|
The warning is, I believe, in error. I meant to file a separate bug on that but got distracted. I imagine the cause is the copy mode on |
Replacing |
Compiles successfully for me with d2ad028
Closing. |
Automatic sync from rustc
The current method for creating the modifies wrapper requires changing the `ensures` clause to have `_renamed` variables which are unsafe copies of the original function arguments. This causes issues with regards to some possible tests as in rust-lang#3239. This change removes the `_renamed` variables and instead simply changes the modifies clauses within the replace to unsafely dereference the pointer to modify the contents of it unsafely, condensing all instances of unsafe Rust into a single location. Resolves rust-lang#3239 Resolves rust-lang#3026 May affect rust-lang#3027. In my attempt to run this example with slight modification to fit the current implementation, I got the error `CBMC appears to have run out of memory. You may want to rerun your proof in an environment with additional memory or use stubbing to reduce the size of the code the verifier reasons about.` This suggests that the compilation is working appropriately but the test case is just too large for CBMC. 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: Matias Scharager <[email protected]>
An LLVM failure results from compiling this program:
The text was updated successfully, but these errors were encountered: