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 foo

Source location: tests/borrowck.rs:2772

fn foo() -> i32 {
    exists<'r0, 'r1> {
        let r: &'r0 i32;
        'a: loop {
            let x: i32 = 0_i32;
            r = &'r1 x;
            break 'a;
        }
        return *r;
    }
}

Rules proved (0)

This test records no positive coverage.

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_statementloopborrow_check_loop(env, assumptions, state, body,… (line 247)9 tests
borrow_check_statementbreakdrop_places(env, assumptions, state, locals_to_d… (line 258)2 tests
borrow_check_statementexistsborrow_check_block(env, assumptions_body, state,… (line 300)21 tests
borrow_check_statementexistsborrow_check_block(env, assumptions_body, state,… (line 311)23 tests
borrow_check_statementexistsborrow_check_block(env, assumptions_body, state,… (line 327)23 tests
borrow_check_looploopborrow_check_block(env, assumptions, state, body… (line 587)9 tests
borrow_check_loopfixed-pointborrow_check_block(env, assumptions, state0, bod… (line 595)9 tests
drop_placesdrop_placesfor_all(place in places) with(state) (access_per… (line 788, blamed at line 789)not counted by the judgment view
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_loanloan is deadloan_not_required_by_live_places(env, assumption… (line 902)23 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_parameteralias-ty RFC 1214loan_not_required_by_parameters(env, assumptions… (line 1362)13 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

Failed proof tree