Open maeiik opened 1 week ago
@jcp19
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 verus_heap::cast
?
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: