Open hayley-leblanc opened 4 months ago
This may be related to https://github.com/verus-lang/verus/issues/657 .
For anyone who encounters this, the current recommended workaround is to move the code into an external function, called by the external_body function:
#[verifier::external]
fn test_maybe_uninit_external() {
let mut maybe_uninit: MaybeUninit<u64> = MaybeUninit::uninit();
let mut bytes: &mut [MaybeUninit<u8>] = maybe_uninit.as_bytes_mut();
let new_bytes: [u8; 8] = [0, 0, 0, 0, 0, 0, 0, 0];
MaybeUninit::write_slice(bytes, &new_bytes);
}
#[verifier::external_body]
#[inline(always)]
fn test_maybe_uninit() {
test_maybe_uninit_external()
}
Hi folks, I'm writing some code involving
MaybeUninit
inexternal_body
functions and have found that Verus is incorrectly checking the bodies of some of these functions. The specific case I encountered involves obtaining a mutable reference to aMaybeUninit
object; attempting to verify anexternal_body
function that does this results in a verification error about&mut
not being supported.An example of such a function that does not verify:
Attempting to verify this function results in
error: The verifier does not yet support the following Rust feature: &mut types, except in special cases
.This does not happen with all
external_body
functions involving mutable references; for example, this function verifies as expected:Both functions are implemented at https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=a677a25cc24042da30e69c076811d4c1
I also noticed that removing
#[verifier::external_body]
fromtest_maybe_uninit()
results in a different error:error: The verifier does not yet support the following Rust feature: &mut dereference in this position (note: &mut dereference is implicit here)