Test `foo`

Source location: tests/borrowck.rs:3869

fn foo() -> u32 {
    exists<'r0, 'r1, 'r2> {
        let x: u32 = 22_u32;
        let p: &'r1 u32 = &'r0 x;
        let q: &'r2 u32 = p;
        x = 1_u32;
        return 0_u32;
    }
}

Rules proved (72)

Judgment	Rule	All tests of this rule
access_kind_for_place_use	move	100 tests
access_permitted	access_permitted	103 tests
access_permitted_by_loan	borrow of disjoint places	41 tests
access_permitted_by_loan	loan is dead	18 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	assign	27 tests
borrow_check_expr	literal	114 tests
borrow_check_expr	place	100 tests
borrow_check_expr	ref	41 tests
borrow_check_expr_has_ty	block	118 tests
borrow_check_place_expr	local	103 tests
borrow_check_statement	exists	48 tests
borrow_check_statement	expr	47 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	feature gate	62 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
loan_cannot_outlive_universal_regions	loan_not_required_by_universal_regions	18 tests
loan_not_required_by_live_places	loan_not_required_by_live_places	18 tests
only_assumed_outlives	existential	43 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	rigid	201 tests
prove_eq	symmetric	220 tests
prove_existential_var_eq	existential-universal	214 tests
prove_outlives	anything can be pending	29 tests
prove_outlives	outlive through assumption	195 tests
prove_outlives	rigid types	55 tests
prove_place_is_movable	local	89 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_list	none	238 tests
prove_predicate_list	some	237 tests
prove_sub	lifetime => outlives	29 tests
prove_sub	rigid	33 tests
prove_wf	integers and booleans	131 tests
prove_wf	references	192 tests
prove_wf	tuples	200 tests
prove_wf	universal variables	206 tests
verify_universal_outlives	verify_universal_outlives	44 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 3521 nodes shown)

How to read this page

Keyboard shortcuts

A MIR Formality

Test foo

Rules proved (72)

Premises failed (0)

Proof trees

Test `foo`