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
The following trait (minimized from the original code):
trait Serializable : Sized {
fn serialized_len() -> (out: u64);
#[verifier::external_body]
fn as_bytes(&self)
{
let ptr = self as *const Self as *const u8;
let slice = unsafe {
std::slice::from_raw_parts(ptr, Self::serialized_len() as usize)
};
}
}
Triggers the following panic:
thread 'rustc' panicked at rust_verify/src/lifetime_generate.rs:1574:38:
no entry found for key
The initial version of the code had as_bytes with a postcondition involving some other Serializable methods and returning a slice; I thought one or both of those things might be related to the panic, but it still occurs in the code shown above with the postcondition and return value removed.
The same error does not occur in a non-default implementation or in a regular function.
Hi all,
The following trait (minimized from the original code):
Triggers the following panic:
The initial version of the code had
as_bytes
with a postcondition involving some otherSerializable
methods and returning a slice; I thought one or both of those things might be related to the panic, but it still occurs in the code shown above with the postcondition and return value removed.The same error does not occur in a non-default implementation or in a regular function.
The code that triggers the panic can also be found here https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=e96b6ad0f673da4557efbba97d07a01b. I've also included a commented-out version of the same trait that does not have a default
as_bytes
implementation + an implementation that do not trigger the panic.The text was updated successfully, but these errors were encountered: