Test `foo`

Source location: tests/mir_typeck.rs:987

fn foo<'a, T>(v1: &'a T) -> T
where
    T: Copy,
    T: 'a,
{
    exists<'r0> {
        let v2: T = *v1;
        return v2;
    }
}

Rules proved (65)

Judgment	Rule	All tests of this rule
access_kind_for_place_use	move	100 tests
access_permitted	access_permitted	103 tests
access_permitted_by_loans	access_permitted_by_loans	106 tests
borrow_check	borrow_check	175 tests
borrow_check_block	basic block	175 tests
borrow_check_expr	place	100 tests
borrow_check_expr_has_ty	block	118 tests
borrow_check_place_expr	deref-ref	42 tests
borrow_check_place_expr	local	103 tests
borrow_check_statement	exists	48 tests
borrow_check_statement	let	94 tests
borrow_check_statement	return	79 tests
check_all_crates	check all prefixes	214 tests
check_associated_ty	check associated ty	195 tests
check_associated_ty_value	check_associated_ty_value	194 tests
check_coherence	check_coherence	214 tests
check_crate	check crate	214 tests
check_crate_item	free fn	175 tests
check_crate_item	trait	214 tests
check_crate_item	trait impl	210 tests
check_drop_impl_always_applicable	not a Drop impl	210 tests
check_fn	check fn	200 tests
check_fn_body	expr fn body	175 tests
check_fn_body	no fn body	192 tests
check_fn_in_trait	check fn in trait	193 tests
check_free_fn	check free fn	175 tests
check_safety_matches	safety matches	210 tests
check_trait	check trait	214 tests
check_trait_impl	check_trait_impl	210 tests
check_trait_impl_item	associated ty value	194 tests
check_trait_item	associated ty in trait	195 tests
check_trait_item	fn in trait	193 tests
drop_places	drop_places	175 tests
is_local_trait_ref	local trait	205 tests
orphan_check	orphan_check	210 tests
overlap_check_impl	different trait	194 tests
overlap_check_impl	not goal	195 tests
overlap_check_impl	same impl	210 tests
prove_after	prove_after	237 tests
prove_assignable	subtype	129 tests
prove_eq	existential	223 tests
prove_eq	normalize-l	26 tests
prove_eq	rigid	201 tests
prove_eq	symmetric	220 tests
prove_existential_var_eq	existential-universal	214 tests
prove_normalize	normalize-via-impl	55 tests
prove_outlives	outlive through assumption	195 tests
prove_place_is_movable	copy	17 tests
prove_place_is_movable	local	89 tests
prove_predicate	assumption	23 tests
prove_predicate	eq	231 tests
prove_predicate	outlives	195 tests
prove_predicate	parameter well formed	204 tests
prove_predicate	positive impl	219 tests
prove_predicate	subtype	134 tests
prove_predicate	trait ref is local	211 tests
prove_predicate	trait well formed	30 tests
prove_predicate_list	none	238 tests
prove_predicate_list	some	237 tests
prove_sub	normalize-l	29 tests
prove_ty_is_copy	trait	20 tests
prove_via	predicate-congruence-axiom	16 tests
prove_wf	references	192 tests
prove_wf	tuples	200 tests
prove_wf	universal variables	206 tests

Premises failed (0)

This test records no negative coverage.

Proof trees

Proof tree

check_all_crates (check all prefixes) mod.rs:55
- args
- for_all mod.rs:42
  - for_all mod.rs:52
    
    args
    
    check_crate (check crate) mod.rs:76
    
    args
    
    for_all mod.rs:61
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait) mod.rs:189
    
    args
    
    check_trait (check trait) traits.rs:25
    
    args
    
    scope traits.rs:9
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args

… (200 of 3696 nodes shown)

How to read this page

Keyboard shortcuts

A MIR Formality

Test foo

Rules proved (65)

Premises failed (0)

Proof trees

Test `foo`