1
Fork 0

Normalize the result of Fields::ty_with_args

We were only instantiating before, which would leak an AliasTy.
I added a test case that reproduce the issue seen here:

https://github.com/model-checking/kani/issues/3113
This commit is contained in:
Celina G. Val 2024-03-28 13:19:50 -07:00
parent d779a7a25f
commit a325bce3cd
3 changed files with 101 additions and 3 deletions

View file

@ -654,7 +654,7 @@ impl AdtDef {
with(|cx| cx.def_ty(self.0))
}
/// Retrieve the type of this Adt instantiating the type with the given arguments.
/// Retrieve the type of this Adt by instantiating and normalizing it with the given arguments.
///
/// This will assume the type can be instantiated with these arguments.
pub fn ty_with_args(&self, args: &GenericArgs) -> Ty {
@ -733,7 +733,7 @@ pub struct FieldDef {
}
impl FieldDef {
/// Retrieve the type of this field instantiating the type with the given arguments.
/// Retrieve the type of this field instantiating and normalizing it with the given arguments.
///
/// This will assume the type can be instantiated with these arguments.
pub fn ty_with_args(&self, args: &GenericArgs) -> Ty {