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

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 (72)

JudgmentRuleAll tests of this rule
access_kind_for_place_usemove100 tests
access_permittedaccess_permitted103 tests
access_permitted_by_loansaccess_permitted_by_loans106 tests
borrow_checkborrow_check175 tests
borrow_check_blockbasic block175 tests
borrow_check_exprcall41 tests
borrow_check_exprplace100 tests
borrow_check_exprtrue28 tests
borrow_check_exprturbofish30 tests
borrow_check_expr_has_tyblock118 tests
borrow_check_fn_reffn-ref43 tests
borrow_check_place_exprlocal103 tests
borrow_check_statementexists48 tests
borrow_check_statementif29 tests
borrow_check_statementlet94 tests
borrow_check_statementreturn79 tests
check_adtcheck adt59 tests
check_all_cratescheck all prefixes214 tests
check_associated_tycheck associated ty195 tests
check_associated_ty_valuecheck_associated_ty_value194 tests
check_coherencecheck_coherence214 tests
check_cratecheck crate214 tests
check_crate_itemadt59 tests
check_crate_itemfeature gate62 tests
check_crate_itemfree fn175 tests
check_crate_itemtrait214 tests
check_crate_itemtrait impl210 tests
check_drop_impl_always_applicablenot a Drop impl210 tests
check_fncheck fn200 tests
check_fn_bodyexpr fn body175 tests
check_fn_bodyno fn body192 tests
check_fn_bodytrusted fn body15 tests
check_fn_in_traitcheck fn in trait193 tests
check_free_fncheck free fn175 tests
check_safety_matchessafety matches210 tests
check_traitcheck trait214 tests
check_trait_implcheck_trait_impl210 tests
check_trait_impl_itemassociated ty value194 tests
check_trait_itemassociated ty in trait195 tests
check_trait_itemfn in trait193 tests
drop_placesdrop_places175 tests
is_local_trait_reflocal trait205 tests
orphan_checkorphan_check210 tests
overlap_check_impldifferent trait194 tests
overlap_check_implnot goal195 tests
overlap_check_implsame impl210 tests
prove_afterprove_after237 tests
prove_assignablesubtype129 tests
prove_eqexistential223 tests
prove_eqrigid201 tests
prove_eqsymmetric220 tests
prove_existential_var_eqexistential-universal214 tests
prove_outlivesanything can be pending29 tests
prove_outlivesoutlive through assumption195 tests
prove_outlivesrigid types55 tests
prove_place_is_movablelocal89 tests
prove_predicateassumption23 tests
prove_predicateeq231 tests
prove_predicateoutlives195 tests
prove_predicateparameter well formed204 tests
prove_predicatepositive impl219 tests
prove_predicatesubtype134 tests
prove_predicatetrait ref is local211 tests
prove_predicate_listnone238 tests
prove_predicate_listsome237 tests
prove_ty_is_rigidrigid76 tests
prove_viarelation-axiom8 tests
prove_wfADT46 tests
prove_wfintegers and booleans131 tests
prove_wfreferences192 tests
prove_wftuples200 tests
prove_wfuniversal variables206 tests

Premises failed (21)

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 135)79 tests
borrow_check_blockbasic blockfor_all(i in 0..stmts.len()) with(env, state) (b… (line 156, blamed at line 157)not counted by the judgment view
borrow_check_statementifborrow_check_block(env, assumptions, state, then… (line 222)2 tests
borrow_check_statementreturnborrow_check_expr(env, assumptions, state, expr,… (line 282)5 tests
borrow_check_statementexistsscope(env.enter_existentially(&with_variables(bi… (line 310, blamed at line 316)not counted by the judgment view
borrow_check_statementexistsscope(env.enter_existentially(&with_variables(bi… (line 324, blamed at line 330)not counted by the judgment view
borrow_check_exprcallborrow_check_expr( env, assumptions, state, call… (line 455)6 tests
borrow_check_exprturbofishborrow_check_fn_ref(env, assumptions, state, id,… (line 566)6 tests
borrow_check_fn_reffn-refprove_where_clauses(env, assumptions, state, whe… (line 632)5 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, Atomi… (line 81)8 tests
check_free_fncheck free fncheck_fn(program, Env::default(), Predicates::t(… (line 24)81 tests
check_fncheck fnscope(enter_universally(env, &f.binder) => (env,… (line 48, blamed at line 54)not counted by the judgment view
check_fn_bodyexpr fn bodyborrow_check(typeck_env, assumptions, initial_st… (line 89)79 tests
check_all_cratescheck all prefixesfor_all(i in 0..crates.len()) (let program = cra… (line 52, blamed at line 54)not counted by the judgment view
check_cratecheck cratefor_all(item in &c.items) (check_crate_item(prog… (line 73, blamed at line 74)not counted by the judgment view
check_crate_itemfree fncheck_free_fn(program, f, crate_id) => () (line 207)81 tests
prove_predicateassumptionprove_via(decls, env, assumptions, a, goal) => c (line 48)34 tests
prove_predicateoutlivesprove_outlives(decls, env, assumptions, a, b) =>… (line 142)8 tests
prove_predicate_listsomeprove_predicate(decls, env, assumptions, wc0) =>… (line 26)67 tests

Proof trees

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

How to read this page