-
Notifications
You must be signed in to change notification settings - Fork 60
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
Unexpected loc SpannedTyped #1197
Comments
Thank you for the report. My first guess is that this is an unsupported feature (but we should be giving you a better error message). But let's diagnose. What's the signature and body of |
It's defined on line 12: #[verifier(external_body)]
pub fn cast<'a, T>(v: &'a Val) -> (r: &'a T) {
unimplemented!()
} |
Sorry I should have read the snippet more carefully. I need to double check when I'm not on mobile, but I think this is an invalid program, but for a different reason: due to the assignment to an immutable reference. It's unfortunate (and indeed a bug) that we panic before we emit that error. I have upcoming changes that should reduce the number of corner cases and make this better. |
I was trying to verify the following (minimized) program using Verus on the main branch (commit edb8f53):
Unfortunately, Verus panics when run with this example:
Our expectation for this example is that Verus would reject this program with a verification error, due to a possible overflow in function
proof_add_one
.verus version:
The text was updated successfully, but these errors were encountered: