-
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
Error: use of undeclared lifetime name #1083
Comments
Yes it looks like a Verus bug. The generated code ought to have the declaration for |
Thanks, that's good to know ! I've put everything in one file and made it even more minimal to make it easier for you to reproduce the bug: use vstd::prelude::*;
pub trait Borrowable {
type Borrowed<'a>;
}
impl Borrowable for u8 {
type Borrowed<'a> = &'a u8;
}
verus! {
#[verifier(reject_recursive_types(T))]
pub struct Container<T: Borrowable>(T);
} Here is the error message: error: use of undeclared lifetime name `'a27_a`
--> src/main.rs:13:40
|
13 | pub struct Container<T: Borrowable>(T);
| ^
error: aborting due to 1 previous error
note: This error was found in Verus pass: ownership checking of tracked code
error: aborting due to 2 previous errors And here is the corresponding content of the variable rust_code from the function checked_tracked_lifetimes in rust_verify/src/lifetime.rs: // ...
trait T25_Borrowable {
type A24_Borrowed;
}
struct D23_Container<A1_T, >(
A1_T,
) where A1_T: T25_Borrowable, ;
impl T25_Borrowable for u8 {
type A24_Borrowed = &'a27_a u8;
} I also tried to add a lifetime to the trait to see if it would solve the problem but it just gave me a new error: use std::marker::PhantomData;
use vstd::prelude::*;
pub trait Borrowable<'a> {
type Borrowed: 'a;
}
impl<'a> Borrowable<'a> for u8 {
type Borrowed = &'a u8;
}
verus! {
#[verifier(reject_recursive_types(T))]
pub struct Container<'a, T: Borrowable<'a>>(T, PhantomData<&'a T>);
} Here is the error: error: missing lifetime specifier
--> src/main.rs:14:48
|
14 | pub struct Container<'a, T: Borrowable<'a>>(T, PhantomData<&'a T>);
| ^
error: aborting due to 1 previous error
note: This error was found in Verus pass: ownership checking of tracked code
error: aborting due to 2 previous errors And here is the corresponding content of the variable rust_code from the function checked_tracked_lifetimes in rust_verify/src/lifetime.rs: // ...
trait T27_Borrowable<'a23_a, > {
type A26_Borrowed : 'a23_a;
}
struct D25_Container<'a23_a, A1_T, >(
A1_T,
D24_PhantomData<&'a23_a A1_T, >,
) where A1_T: T27_Borrowable, A1_T: 'a23_a, ;
struct D24_PhantomData<A1_T, >(
PhantomData<A1_T>,
);
impl<A1_T, > Clone for D24_PhantomData<A1_T, > { fn clone(&self) -> Self { panic!() } }
impl<A1_T, > Copy for D24_PhantomData<A1_T, > {}
impl<'a23_a, > T27_Borrowable<'a23_a, > for u8 {
type A26_Borrowed = &'a23_a u8;
} |
Finally, when I put everything inside the use vstd::prelude::*;
verus! {
pub trait Borrowable {
type Borrowed<'a>;
}
impl Borrowable for u8 {
type Borrowed<'a> = &'a u8;
}
#[verifier(reject_recursive_types(T))]
pub struct Container<T: Borrowable>(T);
} Error: error: The verifier does not yet support the following Rust feature: unsupported generics on associated type
--> src/main.rs:8:5
|
8 | / impl Borrowable for u8 {
9 | | type Borrowed<'a> = &'a u8;
10 | | }
| |_____^
error: aborting due to 1 previous error |
Hi all,
I am currently trying to use Verus to verify Linux Rust kernel modules. When running Verus on the following (minimal) code
I get the following error (the 2 errors reported are exactly the same):
I tried to understand what's going on. When printing the content of the variable
rust_code
from the functionchecked_tracked_lifetimes
inrust_verify/src/lifetime.rs
, I get the following:It thus makes sense that the rustc borrow checker complains about the undeclared lifetime
'a33_a
. However, the above code generated by verus seems wrong to me because the original code contains lifetime annotations fortype Borrowed<'a>
andtype BorrowdMut<'a>
:I am not sure if this is a bug in Verus or if I am missing something. Could you please help me understand what's going on? Thanks in advance!
The text was updated successfully, but these errors were encountered: