You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hi folks, I'm writing some code involving MaybeUninit in external_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 a MaybeUninit object; attempting to verify an external_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 allexternal_body functions involving mutable references; for example, this function verifies as expected:
#[verifier::external_body]
fn test_vec() {
let mut vec = vec![1, 2, 3];
let mut bytes: &mut [u8] = vec.as_mut_slice();
let new_bytes: [u8; 3] = [0, 0, 0];
bytes.copy_from_slice(&new_bytes);
}
I also noticed that removing #[verifier::external_body] from test_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)
The text was updated successfully, but these errors were encountered:
For anyone who encounters this, the current recommended workaround is to move the code into an external function, called by the external_body function:
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)
The text was updated successfully, but these errors were encountered: