Test `foo`

Source location: tests/borrowck.rs:2734

fn foo<'a, 'b>(v1: &'a u32, v2: &'b u32) -> () {
    let output: &'b u32 = v2;
    loop {
        output = v1;
    }
}

Rules proved (0)

This test records no positive coverage.

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.

Judgment	Rule	Premise	All tests of this premise
borrow_check	borrow_check	`borrow_check_block(env, assumptions, state, bloc…` (line 135)	79 tests
borrow_check_block	basic block	`for_all(i in 0..stmts.len()) with(env, state) (b…` (line 156, blamed at line 157)	not counted by the judgment view
borrow_check_statement	expr	`borrow_check_expr( env, assumptions, state, expr…` (line 232)	26 tests
borrow_check_statement	loop	`borrow_check_loop(env, assumptions, state, body,…` (line 249)	9 tests
borrow_check_expr	assign	`prove_assignable(env, assumptions, state, value_…` (line 414)	1 test
borrow_check_loop	loop	`borrow_check_block(env, assumptions, state, body…` (line 652)	9 tests
borrow_check_loop	fixed-point	`borrow_check_block(env, assumptions, state0, bod…` (line 660)	9 tests
prove_assignable	subtype	`prove_sub_type(env, assumptions, state, a, b) =>…` (line 1150)	13 tests
verify_universal_outlives	verify_universal_outlives	`for_all(v in env.env.variables()) (only_assumed_…` (line 19, blamed at line 20)	not counted by the judgment view
only_assumed_outlives	universal lifetime	`for_all(param in transitively_outlived_by(env, o…` (line 48, blamed at line 49)	not counted by the judgment view
can_outlive	universal target	`prove(&env.program, &env.env, assumptions, Atomi…` (line 81)	8 tests
check_free_fn	check free fn	`check_fn(program, Env::default(), Predicates::t(…` (line 24)	81 tests
check_fn	check fn	`scope(enter_universally(env, &f.binder) => (env,…` (line 48, blamed at line 54)	not counted by the judgment view
check_fn_body	expr fn body	`borrow_check(typeck_env, assumptions, initial_st…` (line 89)	79 tests
check_all_crates	check all prefixes	`for_all(i in 0..crates.len()) (let program = cra…` (line 52, blamed at line 54)	not counted by the judgment view
check_crate	check crate	`for_all(item in &c.items) (check_crate_item(prog…` (line 73, blamed at line 74)	not counted by the judgment view
check_crate_item	free fn	`check_free_fn(program, f, crate_id) => ()` (line 207)	81 tests
prove_predicate	outlives	`prove_outlives(decls, env, assumptions, a, b) =>…` (line 142)	8 tests
prove_predicate_list	some	`prove_predicate(decls, env, assumptions, wc0) =>…` (line 26)	67 tests

Proof trees

Failed proof tree

check_all_crates failed mod.rs:42
- args
- rule "check all prefixes" mod.rs:54
  - check_crate failed mod.rs:61
    
    args
    
    rule "check crate" mod.rs:74
    
    check_crate_item failed mod.rs:179
    
    rule "free fn" mod.rs:207
    
    check_free_fn failed fns.rs:14
    
    args
    
    rule "check free fn" fns.rs:24
    
    check_fn failed fns.rs:31
    
    args
    
    rule "check fn" fns.rs:54
    
    check_fn_body failed fns.rs:61
    
    args
    
    rule "expr fn body" fns.rs:89
    
    borrow_check failed nll.rs:124
    
    args
    
    rule "borrow_check" nll.rs:135
    
    borrow_check_block failed nll.rs:142
    
    rule "basic block" nll.rs:157
    
    borrow_check_statement failed nll.rs:174
    
    args
    
    rule "loop" nll.rs:249
    
    borrow_check_loop failed nll.rs:640
    
    args
    
    rule "fixed-point" nll.rs:660
    
    borrow_check_block failed nll.rs:142
    
    args
    
    rule "basic block" nll.rs:157
    
    borrow_check_statement failed nll.rs:174
    
    args
    
    rule "expr" nll.rs:232
    
    borrow_check_expr failed nll.rs:371
    
    args
    
    rule "assign" nll.rs:414
    
    prove_assignable failed nll.rs:1132
    
    args
    
    rule "subtype" nll.rs:1150
    
    verify_universal_outlives failed outlives.rs:8
    
    args
    
    rule "verify_universal_outlives" outlives.rs:20
    
    only_assumed_outlives failed outlives.rs:27
    
    args
    
    rule "universal lifetime" outlives.rs:49
    
    can_outlive failed outlives.rs:56
    
    args
    
    rule "universal target" outlives.rs:81
    
    prove failed outlives.rs:81
    
    args
    
    rule outlives.rs:81
    
    prove_predicate_list failed prove_predicate_list.rs:8
    
    args
    
    rule "some" prove_predicate_list.rs:26
    
    prove_predicate failed prove_predicate.rs:22
    
    args
    
    rule "outlives" prove_predicate.rs:142
    
    prove_outlives failed prove_outlives.rs:8
    
    args
    
    rule "assign" nll.rs:414
    
    prove_assignable failed nll.rs:1132
    
    args
    
    rule "subtype" nll.rs:1150
    
    verify_universal_outlives failed outlives.rs:8
    
    args
    
    rule "verify_universal_outlives" outlives.rs:20
    
    only_assumed_outlives failed outlives.rs:27
    
    args
    
    rule "universal lifetime" outlives.rs:49
    
    can_outlive failed outlives.rs:56
    
    args
    
    rule "universal target" outlives.rs:81
    
    prove failed outlives.rs:81
    
    args
    
    rule outlives.rs:81
    
    prove_predicate_list failed prove_predicate_list.rs:8
    
    args
    
    rule "some" prove_predicate_list.rs:26
    
    prove_predicate failed prove_predicate.rs:22
    
    args
    
    rule "outlives" prove_predicate.rs:142
    
    prove_outlives failed prove_outlives.rs:8
    
    args
    
    rule "loop" nll.rs:652
    
    borrow_check_block failed nll.rs:142
    
    args
    
    rule "basic block" nll.rs:157
    
    borrow_check_statement failed nll.rs:174
    
    args
    
    rule "expr" nll.rs:232
    
    borrow_check_expr failed nll.rs:371
    
    args
    
    rule "assign" nll.rs:414
    
    prove_assignable failed nll.rs:1132
    
    args
    
    rule "subtype" nll.rs:1150
    
    verify_universal_outlives failed outlives.rs:8
    
    args
    
    rule "verify_universal_outlives" outlives.rs:20
    
    only_assumed_outlives failed outlives.rs:27
    
    args
    
    rule "universal lifetime" outlives.rs:49
    
    can_outlive failed outlives.rs:56
    
    args
    
    rule "universal target" outlives.rs:81
    
    prove failed outlives.rs:81
    
    args
    
    rule outlives.rs:81
    
    prove_predicate_list failed prove_predicate_list.rs:8
    
    args
    
    rule "some" prove_predicate_list.rs:26
    
    prove_predicate failed prove_predicate.rs:22
    
    args
    
    rule "outlives" prove_predicate.rs:142
    
    prove_outlives failed prove_outlives.rs:8
    
    args
    
    rule "assign" nll.rs:414
    
    prove_assignable failed nll.rs:1132
    
    args
    
    rule "subtype" nll.rs:1150
    
    verify_universal_outlives failed outlives.rs:8
    
    args
    
    rule "verify_universal_outlives" outlives.rs:20
    
    only_assumed_outlives failed outlives.rs:27
    
    args
    
    rule "universal lifetime" outlives.rs:49
    
    can_outlive failed outlives.rs:56
    
    args
    
    rule "universal target" outlives.rs:81
    
    prove failed outlives.rs:81
    
    args
    
    rule outlives.rs:81
    
    prove_predicate_list failed prove_predicate_list.rs:8
    
    args
    
    rule "some" prove_predicate_list.rs:26
    
    prove_predicate failed prove_predicate.rs:22
    
    args
    
    rule "outlives" prove_predicate.rs:142
    
    prove_outlives failed prove_outlives.rs:8
    
    args
    
    rule "basic block" nll.rs:157
    
    borrow_check_statement failed nll.rs:174
    
    args
    
    rule "loop" nll.rs:249
    
    borrow_check_loop failed nll.rs:640
    
    args
    
    rule "fixed-point" nll.rs:660
    
    borrow_check_block failed nll.rs:142
    
    args
    
    rule "basic block" nll.rs:157
    
    borrow_check_statement failed nll.rs:174
    
    args
    
    rule "expr" nll.rs:232
    
    borrow_check_expr failed nll.rs:371
    
    args
    
    rule "assign" nll.rs:414
    
    prove_assignable failed nll.rs:1132
    
    args
    
    rule "subtype" nll.rs:1150
    
    verify_universal_outlives failed outlives.rs:8
    
    args
    
    rule "verify_universal_outlives" outlives.rs:20
    
    only_assumed_outlives failed outlives.rs:27
    
    args
    
    rule "universal lifetime" outlives.rs:49
    
    can_outlive failed outlives.rs:56
    
    args
    
    rule "universal target" outlives.rs:81
    
    prove failed outlives.rs:81
    
    args
    
    rule outlives.rs:81
    
    prove_predicate_list failed prove_predicate_list.rs:8
    
    args
    
    rule "some" prove_predicate_list.rs:26
    
    prove_predicate failed prove_predicate.rs:22
    
    args
    
    rule "outlives" prove_predicate.rs:142
    
    prove_outlives failed prove_outlives.rs:8
    
    args
    
    rule "assign" nll.rs:414
    
    prove_assignable failed nll.rs:1132
    
    args
    
    rule "subtype" nll.rs:1150
    
    verify_universal_outlives failed outlives.rs:8
    
    args
    
    rule "verify_universal_outlives" outlives.rs:20
    
    only_assumed_outlives failed outlives.rs:27
    
    args
    
    rule "universal lifetime" outlives.rs:49
    
    can_outlive failed outlives.rs:56
    
    args
    
    rule "universal target" outlives.rs:81
    
    prove failed outlives.rs:81
    
    args
    
    rule outlives.rs:81
    
    prove_predicate_list failed prove_predicate_list.rs:8
    
    args
    
    rule "some" prove_predicate_list.rs:26
    
    prove_predicate failed prove_predicate.rs:22
    
    args
    
    rule "outlives" prove_predicate.rs:142
    
    prove_outlives failed prove_outlives.rs:8
    
    args
    
    rule "loop" nll.rs:652
    
    borrow_check_block failed nll.rs:142
    
    args
    
    rule "basic block" nll.rs:157
    
    borrow_check_statement failed nll.rs:174
    
    args
    
    rule "expr" nll.rs:232
    
    borrow_check_expr failed nll.rs:371
    
    args
    
    rule "assign" nll.rs:414
    
    prove_assignable failed nll.rs:1132
    
    args
    
    rule "subtype" nll.rs:1150
    
    verify_universal_outlives failed outlives.rs:8
    
    args
    
    rule "verify_universal_outlives" outlives.rs:20
    
    only_assumed_outlives failed outlives.rs:27
    
    args
    
    rule "universal lifetime" outlives.rs:49
    
    can_outlive failed outlives.rs:56
    
    args
    
    rule "universal target" outlives.rs:81
    
    prove failed outlives.rs:81
    
    args
    
    rule outlives.rs:81
    
    prove_predicate_list failed prove_predicate_list.rs:8
    
    args
    
    rule "some" prove_predicate_list.rs:26
    
    prove_predicate failed prove_predicate.rs:22
    
    args
    
    rule "outlives" prove_predicate.rs:142
    
    prove_outlives failed prove_outlives.rs:8
    
    args
    
    rule "assign" nll.rs:414
    
    prove_assignable failed nll.rs:1132
    
    args
    
    rule "subtype" nll.rs:1150
    
    verify_universal_outlives failed outlives.rs:8
    
    args
    
    rule "verify_universal_outlives" outlives.rs:20
    
    only_assumed_outlives failed outlives.rs:27
    
    args
    
    rule "universal lifetime" outlives.rs:49
    
    can_outlive failed outlives.rs:56
    
    args
    
    rule "universal target" outlives.rs:81
    
    prove failed outlives.rs:81
    
    args
    
    rule outlives.rs:81
    
    prove_predicate_list failed prove_predicate_list.rs:8
    
    args
    
    rule "some" prove_predicate_list.rs:26
    
    prove_predicate failed prove_predicate.rs:22
    
    args
    
    rule "outlives" prove_predicate.rs:142
    
    prove_outlives failed prove_outlives.rs:8
    
    args

How to read this page

A MIR Formality

Test `foo`

Rules proved (0)

Premises failed (19)

Proof trees

Keyboard shortcuts

A MIR Formality

Test foo

Rules proved (0)

Premises failed (19)

Proof trees

Test `foo`