-
Notifications
You must be signed in to change notification settings - Fork 352
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
Does this code violate the alias model? #3921
Comments
This code seems perfectly valid to me. It's confusing because of the way the source is written, but I think that's it. Operationally it is much simpler. Roughly line-by-line: We create a raw pointer which definitely has read permission to Perhaps what is tripping you up is that the aliasing model does not follow pointer indirection? If you have a |
The problem is that, from callee's perspective, it's just a |
I've explained how the above code works in Stacked Borrows, and that the fact that this passes is not a bug in Miri. Now you're trying to argue that this has optimization value and should be UB, which is a completely different discussion. This is related to but probably not exactly the same as rust-lang/unsafe-code-guidelines#412. You should try to argue for this optimization in an issue on that repo. |
come here from rust-lang/rust#130853
here is simplified code, which can be successfully run by miri
Does this code conform to the alias model? Or miri has some issues with handling
cast
?The text was updated successfully, but these errors were encountered: