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:638

fn foo() -> Datum {
    exists<'r0, 'r1> {
        let x: Datum = Datum { value: 0_u32 };
        let r: &'r0 Datum = &'r1 x;
        let y: Datum = *r;
        return y;
    }
}

Rules proved (0)

This test records no positive coverage.

Premises failed (26)

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_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_expr_has_tyblockborrow_check_expr(env, assumptions, state, expr,… (line 364)28 tests
borrow_check_exprplaceprove_place_is_movable(env, assumptions, state, … (line 506)3 tests
prove_ty_is_copytraitenv.prove_goal(assumptions, &state, goal) => sta… (line 968)3 tests
prove_place_is_movablecopyprove_ty_is_copy(env, assumptions, state, &place… (line 1013)3 tests
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
prove_afterprove_afterprove(decls, c1.env(), assumptions, goal) => c2 (line 19)18 tests
prove_eqsymmetricprove_eq(decls, env, assumptions, r, l) => env_c (line 38)15 tests
prove_eqnormalize-lprove_normalize(decls, env, assumptions, x) => C… (line 68)15 tests
prove_eqnormalize-lprove_after(decls, c, assumptions, eq(y, z)) => … (line 69)3 tests
prove_normalizenormalize-via-assumptionprove_normalize_via(decls, env, assumptions, a, … (line 32)10 tests
prove_wcassumptionprove_via(decls, env, assumptions, a, goal) => c (line 48)21 tests
prove_wcpositive implprove(decls, env, co_assumptions, Wcs::all_eq(&t… (line 73)7 tests
prove_wctrait implied boundti in decls.trait_invariants() (line 109)14 tests
prove_wceqprove_eq(decls, env, assumptions, a, b) => c (line 119)15 tests
prove_wc_listsomeprove_wc(decls, env, assumptions, wc0) => c (line 26)42 tests

Proof trees

Failed proof tree
… (200 of 1236 nodes shown)