Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Positive coverage: check_drop_impl_always_applicable / Drop impl is always applicable

Drop impl is always applicable
LineCoverageSource
318✗(if **trait_impl.trait_id() == *"Drop")
3201(let adt_id = drop_impl_adt_id(&trait_impl)?)
3221(check_drop_impl_in_defining_crate(program, adt_id, crate_id) => ())
323✗(let adt = program.program().adt_item_named(adt_id)?.to_adt())
325N/A(let (env, adt_vars) = Env::default().universal_substitution(&adt.binder))
326✗(let adt_bound = adt.binder.instantiate_with(adt_vars)?)
327N/A(let adt_self_ty = Ty::rigid(adt_id, adt_vars))
330N/A(let drop_trait_ref = crate::grammar::TraitId::new("Drop").with(adt_self_ty, ()))
3313(super::prove_goal(&program, &env, &adt_bound.where_clauses,
Predicate::IsImplemented(drop_trait_ref.clone())) => ())
──────── ("Drop impl is always applicable")
3346(check_drop_impl_always_applicable(program, trait_impl, crate_id) => ())

6 tests exercised this rule:

Source location: tests/drop.rs:20

#[test]
fn drop_impl_simple_struct() {
    FormalityTest::new(crates![
        crate Foo {
            struct MyStruct {
                value: u32,
            }

            impl Drop for MyStruct {}
        }
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1058 nodes shown)

Source location: tests/drop.rs:38

#[test]
fn drop_impl_generic_struct() {
    FormalityTest::new(crates![
        crate Foo {
            trait Clone {}

            struct MyStruct<T> where T: Clone {
                value: T,
            }

            impl<T> Drop for MyStruct<T> where T: Clone {}
        }
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1108 nodes shown)

Source location: tests/drop.rs:54

#[test]
fn drop_impl_generic_no_where_clauses() {
    FormalityTest::new(crates![
        crate Foo {
            struct Wrapper<T> {
                value: T,
            }

            impl<T> Drop for Wrapper<T> {}
        }
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1074 nodes shown)

Source location: tests/drop.rs:78

#[test]
fn drop_impl_subset_where_clauses() {
    FormalityTest::new(crates![
        crate Foo {
            trait Clone {}
            trait Debug {}

            struct MyStruct<T> where T: Clone, T: Debug {
                value: T,
            }

            // Impl has no where-clauses — but the struct requires them.
            impl<T> Drop for MyStruct<T> {}
        }
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1096 nodes shown)

Source location: tests/drop.rs:94

#[test]
fn drop_impl_enum() {
    FormalityTest::new(crates![
        crate Foo {
            enum MyEnum {
                Variant{},
            }

            impl Drop for MyEnum {}
        }
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1049 nodes shown)

Source location: tests/drop.rs:111

#[test]
fn drop_impl_cross_crate_local() {
    FormalityTest::new(crates![
        crate a {
            struct MyStruct {
                value: u32,
            }

            impl Drop for MyStruct {}
        },
        crate b {}
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1061 nodes shown)