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.

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

Fix slice with range encoding #972

Merged
merged 6 commits into from
May 27, 2022

Conversation

JonasAlaif
Copy link
Contributor

Fixes #960
Issue is described there. Not sure if this is the correct way to do the error reporting?
It would be really nice to just have a contract for index and index_mut and report the error as a precondition violation of those. E.g. I really don't want to hardcode the pledge required for index_mut by hand.

@JonasAlaif JonasAlaif requested a review from fpoli April 22, 2022 14:15
Copy link
Member

@fpoli fpoli left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The error reporting looks good to me. I left a comment.

@JonasAlaif
Copy link
Contributor Author

bors r+

bors bot pushed a commit that referenced this pull request Apr 27, 2022
Fixes #960
Issue is described there. Not sure if this is the correct way to do the error reporting?
It would be really nice to just have a contract for `index` and `index_mut` and report the error as a precondition violation of those. E.g. I really don't want to hardcode the pledge required for `index_mut` by hand.
@bors
Copy link
Contributor

bors bot commented Apr 27, 2022

Build failed:

@JonasAlaif
Copy link
Contributor Author

bors r+

bors bot pushed a commit that referenced this pull request Apr 28, 2022
Fixes #960
Issue is described there. Not sure if this is the correct way to do the error reporting?
It would be really nice to just have a contract for `index` and `index_mut` and report the error as a precondition violation of those. E.g. I really don't want to hardcode the pledge required for `index_mut` by hand.
@bors
Copy link
Contributor

bors bot commented Apr 28, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Apr 28, 2022
Fixes #960
Issue is described there. Not sure if this is the correct way to do the error reporting?
It would be really nice to just have a contract for `index` and `index_mut` and report the error as a precondition violation of those. E.g. I really don't want to hardcode the pledge required for `index_mut` by hand.
@bors
Copy link
Contributor

bors bot commented Apr 29, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Apr 29, 2022
Fixes #960
Issue is described there. Not sure if this is the correct way to do the error reporting?
It would be really nice to just have a contract for `index` and `index_mut` and report the error as a precondition violation of those. E.g. I really don't want to hardcode the pledge required for `index_mut` by hand.
@bors
Copy link
Contributor

bors bot commented Apr 29, 2022

Build failed:

@JonasAlaif
Copy link
Contributor Author

bors r+

@bors
Copy link
Contributor

bors bot commented May 27, 2022

@bors bors bot merged commit 5a3f296 into viperproject:master May 27, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Prusti unexpected internal error
2 participants