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
347✗(if **trait_impl.trait_id() == *"Drop")
3491(let adt_id = drop_impl_adt_id(&trait_impl)?)
3511(check_drop_impl_in_defining_crate(program, adt_id, crate_id) => ())
352✗(let adt = program.program().adt_item_named(adt_id)?.to_adt())
354✗(scope(enter_universally(Env::default(), &with_variables(&adt.binder))
=> (env, (adt_parameters, AdtBoundData { where_clauses, variants: _ }))) with()
(let adt_self_ty = Ty::rigid(adt_id, adt_parameters))
// Prove: under the ADT's where-clauses, Drop is implemented for the ADT.
// This will find the impl, unify its self type, and verify its where-clauses.
(let drop_trait_ref = crate::grammar::TraitId::new("Drop").with(adt_self_ty, ()))
(super::prove_goal(program, env, where_clauses,
AtomicPredicate::is_implemented(drop_trait_ref)) => ()))
──────── ("Drop impl is always applicable")
3635(check_drop_impl_always_applicable(program, trait_impl, crate_id) => ())

5 tests exercised this rule:

Source location: tests/drop.rs:23 (all coverage from this test)

Proof tree
… (200 of 3538 nodes shown)

Source location: tests/drop.rs:43 (all coverage from this test)

Proof tree
… (200 of 3630 nodes shown)

Source location: tests/drop.rs:61 (all coverage from this test)

Proof tree
… (200 of 3579 nodes shown)

Source location: tests/drop.rs:108 (all coverage from this test)

Proof tree
… (200 of 3529 nodes shown)

Source location: tests/drop.rs:128 (all coverage from this test)

Proof tree
… (200 of 3541 nodes shown)

How to read this page