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 use_it

Source location: tests/borrowck.rs:4472

fn use_it<'a, 'b>() -> u32 {
    exists<'r0> {
        let v: Invariant<'r0> = create_invariant::<'r0>();
        if true {
            return sink::<'a, 'r0>(v);
        } else {
            return sink::<'b, 'r0>(v);
        }
    }
}

Rules proved (67)

JudgmentRuleAll tests of this rule
access_kind_for_place_usemove71 tests
access_permittedaccess_permitted73 tests
access_permitted_by_loansaccess_permitted_by_loans76 tests
borrow_checkborrow_check90 tests
borrow_check_blockbasic block90 tests
borrow_check_exprcall25 tests
borrow_check_exprplace71 tests
borrow_check_exprtrue27 tests
borrow_check_exprturbofish19 tests
borrow_check_expr_has_tyblock72 tests
borrow_check_place_exprlocal73 tests
borrow_check_statementexists36 tests
borrow_check_statementif28 tests
borrow_check_statementlet70 tests
borrow_check_statementreturn64 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_fn_bodytrusted fn body12 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
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-universal132 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_ty_is_rigidrigid33 tests
prove_viarelation-axiom6 tests
prove_wcassumption19 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_wfintegers and booleans97 tests
prove_wfreferences41 tests
prove_wfuniversal variables124 tests

Premises failed (19)

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_statementifborrow_check_block(env, assumptions, state, then… (line 220)2 tests
borrow_check_statementreturnborrow_check_expr(env, assumptions, state, expr,… (line 280)5 tests
borrow_check_statementexistsverify_universal_outlives(env, assumptions_body,… (line 315)1 test
borrow_check_statementexistsborrow_check_block(env, assumptions_body, state,… (line 330)6 tests
borrow_check_exprcallprove_where_clauses(env, assumptions, state, whe… (line 445)2 tests
verify_universal_outlivesverify_universal_outlivesfor_all(v in env.env.variables()) (only_assumed_… (line 19, blamed at line 20)not counted by the judgment view
only_assumed_outlivesuniversal lifetimefor_all(param in transitively_outlived_by(env, o… (line 48, blamed at line 49)not counted by the judgment view
can_outliveuniversal targetprove(&env.program, &env.env, assumptions, Predi… (line 81)7 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_wcassumptionprove_via(decls, env, assumptions, a, goal) => c (line 48)21 tests
prove_wcoutlivesprove_outlives(decls, env, assumptions, a, b) =>… (line 146)7 tests
prove_wc_listsomeprove_wc(decls, env, assumptions, wc0) => c (line 26)42 tests

Proof trees

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