Test `foo`

Source location: tests/borrowck.rs:1476

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

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	let	`borrow_check_expr_has_ty(env, assumptions, state…` (line 189)	36 tests
borrow_check_statement	exists	`scope(env.enter_existentially(&with_variables(bi…` (line 300, blamed at line 302)	not counted by the judgment view
borrow_check_statement	exists	`scope(env.enter_existentially(&with_variables(bi…` (line 310, blamed at line 312)	not counted by the judgment view
borrow_check_statement	exists	`scope(env.enter_existentially(&with_variables(bi…` (line 324, blamed at line 327)	not counted by the judgment view
borrow_check_expr_has_ty	block	`borrow_check_expr(env, assumptions, state, expr,…` (line 363)	36 tests
borrow_check_expr	place	`prove_place_is_movable(env, assumptions, state, …` (line 549)	3 tests
prove_ty_is_copy	trait	`env.prove_goal(assumptions, &state, goal) => sta…` (line 1033)	3 tests
prove_place_is_movable	copy	`prove_ty_is_copy(env, assumptions, state, &place…` (line 1078)	3 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_after	prove_after	`prove(decls, c1.env(), assumptions, goal) => c2` (line 19)	21 tests
prove_eq	symmetric	`prove_eq(decls, env, assumptions, r, l) => env_c` (line 38)	17 tests
prove_eq	normalize-l	`prove_normalize(decls, env, assumptions, x) => C…` (line 68)	17 tests
prove_eq	normalize-l	`prove_after(decls, c, assumptions, eq(y, z)) => …` (line 69)	3 tests
prove_normalize	normalize-via-assumption	`prove_normalize_via(decls, env, assumptions, a, …` (line 36)	14 tests
prove_predicate	assumption	`prove_via(decls, env, assumptions, a, goal) => c` (line 48)	34 tests
prove_predicate	positive impl	`scope(enter_existentially_with_constraints(env, …` (line 60, blamed at line 71)	not counted by the judgment view
prove_predicate	trait implied bound	`ti in decls.trait_invariants()` (line 106)	19 tests
prove_predicate	eq	`prove_eq(decls, env, assumptions, a, b) => c` (line 115)	17 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 "exists" nll.rs:302
    
    borrow_check_block failed nll.rs:142
    
    args
    
    rule "basic block" nll.rs:157
    
    borrow_check_statement failed nll.rs:174
    
    args
    
    rule "let" nll.rs:189
    
    borrow_check_expr_has_ty failed nll.rs:350
    
    args
    
    rule "block" nll.rs:363
    
    borrow_check_expr failed nll.rs:371
    
    args
    
    rule "place" nll.rs:549
    
    prove_place_is_movable failed nll.rs:1040
    
    args
    
    rule "copy" nll.rs:1078
    
    prove_ty_is_copy failed nll.rs:1021
    
    rule "trait" nll.rs:1033
    
    prove failed function.rs:250
    
    args
    
    rule function.rs:250
    
    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 "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "positive impl" prove_predicate.rs:71
    
    prove failed prove_predicate.rs:71
    
    args
    
    rule prove_predicate.rs:71
    
    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 "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "eq" prove_predicate.rs:115
    
    prove_eq failed prove_eq.rs:23
    
    args
    
    rule "normalize-l" prove_eq.rs:69
    
    prove_after failed prove_after.rs:8
    
    args
    
    rule "prove_after" prove_after.rs:19
    
    prove failed prove_after.rs:19
    
    args
    
    rule prove_after.rs:19
    
    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 "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "eq" prove_predicate.rs:115
    
    prove_eq failed prove_eq.rs:23
    
    args
    
    rule "normalize-l" prove_eq.rs:68
    
    prove_normalize failed prove_normalize.rs:22
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "symmetric" prove_eq.rs:38
    
    prove_eq failed prove_eq.rs:23
    
    args
    
    rule "normalize-l" prove_eq.rs:68
    
    prove_normalize failed prove_normalize.rs:22
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-l" prove_eq.rs:69
    
    prove_after failed prove_after.rs:8
    
    args
    
    rule "prove_after" prove_after.rs:19
    
    prove failed prove_after.rs:19
    
    args
    
    rule prove_after.rs:19
    
    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 "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "eq" prove_predicate.rs:115
    
    prove_eq failed prove_eq.rs:23
    
    args
    
    rule "normalize-l" prove_eq.rs:68
    
    prove_normalize failed prove_normalize.rs:22
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "symmetric" prove_eq.rs:38
    
    prove_eq failed prove_eq.rs:23
    
    args
    
    rule "normalize-l" prove_eq.rs:68
    
    prove_normalize failed prove_normalize.rs:22
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "symmetric" prove_eq.rs:38
    
    prove_eq failed prove_eq.rs:23
    
    args
    
    rule "normalize-l" prove_eq.rs:68
    
    prove_normalize failed prove_normalize.rs:22
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "positive impl" prove_predicate.rs:71
    
    prove failed prove_predicate.rs:71
    
    args
    
    rule prove_predicate.rs:71
    
    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 "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "eq" prove_predicate.rs:115
    
    prove_eq failed prove_eq.rs:23
    
    args
    
    rule "normalize-l" prove_eq.rs:69
    
    prove_after failed prove_after.rs:8
    
    args
    
    rule "prove_after" prove_after.rs:19
    
    prove failed prove_after.rs:19
    
    args
    
    rule prove_after.rs:19
    
    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 "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "eq" prove_predicate.rs:115
    
    prove_eq failed prove_eq.rs:23
    
    args
    
    rule "normalize-l" prove_eq.rs:68
    
    prove_normalize failed prove_normalize.rs:22
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "symmetric" prove_eq.rs:38
    
    prove_eq failed prove_eq.rs:23
    
    args
    
    rule "normalize-l" prove_eq.rs:68
    
    prove_normalize failed prove_normalize.rs:22
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-l" prove_eq.rs:69
    
    prove_after failed prove_after.rs:8
    
    args
    
    rule "prove_after" prove_after.rs:19
    
    prove failed prove_after.rs:19
    
    args
    
    rule prove_after.rs:19
    
    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 "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "assumption" prove_predicate.rs:48
    
    prove_via failed prove_via.rs:9
    
    args
    
    rule "eq" prove_predicate.rs:115
    
    prove_eq failed prove_eq.rs:23
    
    args
    
    rule "normalize-l" prove_eq.rs:68
    
    prove_normalize failed prove_normalize.rs:22
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36
    
    prove_normalize_via failed prove_normalize.rs:55
    
    args
    
    rule "normalize-via-assumption" prove_normalize.rs:36

… (200 of 1420 nodes shown)

How to read this page

A MIR Formality

Test `foo`

Rules proved (0)

Premises failed (26)

Proof trees

Keyboard shortcuts

A MIR Formality

Test foo

Rules proved (0)

Premises failed (26)

Proof trees

Test `foo`