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

Test min_problem_case_3

Source location: tests/borrowck.rs:2158

fn min_problem_case_3<'a>(m: &'a mut Map) -> &'a mut Map {
    exists<'r0, 'r1> {
        let n: &'r0 mut Map = &'r0 mut *m;
        if true {
            return n;
        } else {
            let o: &'r1 mut Map = &'r1 mut *m;
            return o;
        }
    }
}

Rules proved (81)

JudgmentRuleAll tests of this rule
access_kind_for_place_usemove71 tests
access_permittedaccess_permitted73 tests
access_permitted_by_loanborrow of disjoint places29 tests
access_permitted_by_loanloan is dead15 tests
access_permitted_by_loansaccess_permitted_by_loans76 tests
borrow_checkborrow_check90 tests
borrow_check_blockbasic block90 tests
borrow_check_exprplace71 tests
borrow_check_exprref29 tests
borrow_check_exprtrue27 tests
borrow_check_expr_has_tyblock72 tests
borrow_check_place_exprderef-ref30 tests
borrow_check_place_exprlocal73 tests
borrow_check_statementexists36 tests
borrow_check_statementif28 tests
borrow_check_statementlet70 tests
borrow_check_statementreturn64 tests
can_outliveexistential target19 tests
check_adtcheck adt45 tests
check_all_cratescheck all prefixes131 tests
check_associated_tycheck associated ty116 tests
check_associated_ty_valuecheck_associated_ty_value115 tests
check_coherencecheck_coherence131 tests
check_cratecheck crate131 tests
check_crate_itemadt45 tests
check_crate_itemfeature gate45 tests
check_crate_itemfree fn94 tests
check_crate_itemtrait131 tests
check_crate_itemtrait impl127 tests
check_drop_impl_always_applicablenot a Drop impl127 tests
check_fncheck fn96 tests
check_fn_bodyexpr fn body90 tests
check_free_fncheck free fn94 tests
check_safety_matchessafety matches127 tests
check_traitcheck trait131 tests
check_trait_implcheck_trait_impl127 tests
check_trait_impl_itemassociated ty value115 tests
check_trait_itemassociated ty in trait116 tests
drop_placesdrop_places90 tests
is_local_trait_reflocal trait126 tests
loan_cannot_outliveloan_cannot_outlive8 tests
loan_cannot_outlive_universal_regionsloan_not_required_by_universal_regions15 tests
loan_not_required_by_live_placeloan is not required by type10 tests
loan_not_required_by_live_place_prefixno prefix10 tests
loan_not_required_by_live_placesloan_not_required_by_live_places15 tests
loan_not_required_by_parameterlifetime8 tests
loan_not_required_by_parameterrigid-ty10 tests
loan_not_required_by_parametersloan_not_required_by_parameters10 tests
only_assumed_outlivesexistential31 tests
only_assumed_outlivesuniversal lifetime24 tests
orphan_checkorphan_check127 tests
overlap_checknot_goal115 tests (not in the report)
overlap_checkskip_different_trait115 tests (not in the report)
overlap_checkskip_same_impl127 tests (not in the report)
prove_afterprove_after154 tests
prove_assignablesubtype82 tests
prove_eqexistential141 tests
prove_eqrigid119 tests
prove_eqsymmetric138 tests
prove_existential_var_eqexistential-nonvar43 tests
prove_existential_var_eqexistential-universal132 tests
prove_normalizenormalize-via-impl39 tests
prove_outlivesanything can be pending28 tests (not in the report)
prove_outlivesoutlive through assumption113 tests (not in the report)
prove_outlivesrigid types39 tests (not in the report)
prove_place_is_movablelocal68 tests
prove_sublifetime => outlives28 tests
prove_subnormalize-l25 tests
prove_subrigid31 tests
prove_wceq148 tests
prove_wcoutlives113 tests
prove_wcparameter well formed121 tests
prove_wcpositive impl136 tests
prove_wcsubtype82 tests
prove_wctrait ref is local128 tests
prove_wc_listnone155 tests
prove_wc_listsome154 tests
prove_wfADT32 tests
prove_wfreferences41 tests
prove_wfuniversal variables124 tests
verify_universal_outlivesverify_universal_outlives32 tests

Premises failed (27)

The last column links to the premise’s page when the judgment view counts this failure against that premise. It does not when the premise is read as infallible, or when the failure was blamed inside a multi-line premise that carries no record on its own first line.

JudgmentRulePremiseAll tests of this premise
borrow_checkborrow_checkborrow_check_block(env, assumptions, state, bloc… (line 138)60 tests
borrow_check_blockbasic blockfor_all(i in 0..stmts.len()) with(env, state) (b… (line 159, blamed at line 160)not counted by the judgment view
borrow_check_statementletfor_all(init in init.into_iter()) with (state) /… (line 192, blamed at line 194)not counted by the judgment view
borrow_check_statementifborrow_check_block(env, assumptions, state, &els… (line 221)3 tests
borrow_check_statementexistsborrow_check_block(env, assumptions_body, state,… (line 330)6 tests
borrow_check_expr_has_tyblockborrow_check_expr(env, assumptions, state, expr,… (line 364)28 tests
borrow_check_exprrefaccess_permitted( env, assumptions, state, Acces… (line 478)7 tests
access_permittedaccess_permittedaccess_permitted_by_loans(env, assumptions, stat… (line 813)18 tests
access_permitted_by_loansaccess_permitted_by_loansfor_all(loan in &state.current.loans_live) with(… (line 832, blamed at line 833)not counted by the judgment view
access_permitted_by_loanborrow of disjoint placesif place_disjoint_from_place(&loan.place, &acces… (line 855)23 tests
access_permitted_by_loanwrite-indirectif let TypedPlaceExpressionData::Deref(place_loa… (line 882)21 tests
access_permitted_by_loanwrite-indirectif place_accessed.is_prefix_of(place_loaned_ref) (line 884)7 tests
access_permitted_by_loanloan is deadloan_not_required_by_live_places(env, assumption… (line 902)23 tests
loan_cannot_outlive_universal_regionsloan_not_required_by_universal_regionsif outlived_by_loan.iter().all(|p| match p { // … (line 1197)5 tests
loan_not_required_by_live_placesloan_not_required_by_live_placesfor_all(live_place in places_live_after_access) … (line 1249, blamed at line 1251)not counted by the judgment view
loan_not_required_by_live_placeloan is not required by typeloan_not_required_by_parameter(env, assumptions,… (line 1278)23 tests
loan_not_required_by_parameterrigid-tyloan_not_required_by_parameters(env, assumptions… (line 1346)23 tests
loan_not_required_by_parameteruniversal-variableloan_cannot_outlive_universal_regions(env, assum… (line 1420)5 tests
loan_not_required_by_parameterlifetimeloan_cannot_outlive(env, assumptions, outlives, … (line 1436)23 tests
loan_cannot_outliveloan_cannot_outliveif !outlived_by_loan.contains(&lifetime.upcast()… (line 1456)23 tests
loan_not_required_by_parametersloan_not_required_by_parametersfor_all(param in live_parameters) (loan_not_requ… (line 1483, blamed at line 1484)not counted by the judgment view
check_free_fncheck free fncheck_fn(program, Env::default(), Wcs::t(), f, c… (line 24)61 tests
check_fncheck fncheck_fn_body(program, env, assumptions, body, i… (line 55)60 tests
check_fn_bodyexpr fn bodyborrow_check(typeck_env, assumptions, initial_st… (line 90)60 tests
check_all_cratescheck all prefixesfor_all(i in 0..crates.len()) (let program = cra… (line 51, blamed at line 53)not counted by the judgment view
check_cratecheck cratefor_all(item in &c.items) (check_crate_item(prog… (line 72, blamed at line 73)not counted by the judgment view
check_crate_itemfree fncheck_free_fn(program, f, crate_id) => () (line 206)61 tests

Proof trees

Proof tree
… (200 of 1350 nodes shown)
Failed proof tree