Test foo
Source location: tests/borrowck.rs:2772
fn foo() -> i32 {
exists<'r0, 'r1> {
let r: &'r0 i32;
'a: loop {
let x: i32 = 0_i32;
r = &'r1 x;
break 'a;
}
return *r;
}
}
Rules proved (0)
This test records no positive coverage.
Premises failed (27)
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 138) | 60 tests |
| borrow_check_block | basic block | for_all(i in 0..stmts.len()) with(env, state) (b… (line 159, blamed at line 160) | not counted by the judgment view |
| borrow_check_statement | loop | borrow_check_loop(env, assumptions, state, body,… (line 247) | 9 tests |
| borrow_check_statement | break | drop_places(env, assumptions, state, locals_to_d… (line 258) | 2 tests |
| borrow_check_statement | exists | borrow_check_block(env, assumptions_body, state,… (line 300) | 21 tests |
| borrow_check_statement | exists | borrow_check_block(env, assumptions_body, state,… (line 311) | 23 tests |
| borrow_check_statement | exists | borrow_check_block(env, assumptions_body, state,… (line 327) | 23 tests |
| borrow_check_loop | loop | borrow_check_block(env, assumptions, state, body… (line 587) | 9 tests |
| borrow_check_loop | fixed-point | borrow_check_block(env, assumptions, state0, bod… (line 595) | 9 tests |
| drop_places | drop_places | for_all(place in places) with(state) (access_per… (line 788, blamed at line 789) | not counted by the judgment view |
| access_permitted_by_loans | access_permitted_by_loans | for_all(loan in &state.current.loans_live) with(… (line 832, blamed at line 833) | not counted by the judgment view |
| access_permitted_by_loan | borrow of disjoint places | if place_disjoint_from_place(&loan.place, &acces… (line 855) | 23 tests |
| access_permitted_by_loan | write-indirect | if let TypedPlaceExpressionData::Deref(place_loa… (line 882) | 21 tests |
| access_permitted_by_loan | loan is dead | loan_not_required_by_live_places(env, assumption… (line 902) | 23 tests |
| loan_not_required_by_live_places | loan_not_required_by_live_places | for_all(live_place in places_live_after_access) … (line 1249, blamed at line 1251) | not counted by the judgment view |
| loan_not_required_by_live_place | loan is not required by type | loan_not_required_by_parameter(env, assumptions,… (line 1278) | 23 tests |
| loan_not_required_by_parameter | rigid-ty | loan_not_required_by_parameters(env, assumptions… (line 1346) | 23 tests |
| loan_not_required_by_parameter | alias-ty RFC 1214 | loan_not_required_by_parameters(env, assumptions… (line 1362) | 13 tests |
| loan_not_required_by_parameter | lifetime | loan_cannot_outlive(env, assumptions, outlives, … (line 1436) | 23 tests |
| loan_cannot_outlive | loan_cannot_outlive | if !outlived_by_loan.contains(&lifetime.upcast()… (line 1456) | 23 tests |
| loan_not_required_by_parameters | loan_not_required_by_parameters | for_all(param in live_parameters) (loan_not_requ… (line 1483, blamed at line 1484) | not counted by the judgment view |
| check_free_fn | check free fn | check_fn(program, Env::default(), Wcs::t(), f, c… (line 24) | 61 tests |
| check_fn | check fn | check_fn_body(program, env, assumptions, body, i… (line 55) | 60 tests |
| check_fn_body | expr fn body | borrow_check(typeck_env, assumptions, initial_st… (line 90) | 60 tests |
| check_all_crates | check all prefixes | for_all(i in 0..crates.len()) (let program = cra… (line 51, blamed at line 53) | not counted by the judgment view |
| check_crate | check crate | for_all(item in &c.items) (check_crate_item(prog… (line 72, blamed at line 73) | not counted by the judgment view |
| check_crate_item | free fn | check_free_fn(program, f, crate_id) => () (line 206) | 61 tests |
Proof trees
Failed proof tree
check_all_crates failedmod.rs:41args
rule "check all prefixes"mod.rs:53check_crate failedmod.rs:60args
rule "check crate"mod.rs:73check_crate_item failedmod.rs:178rule "free fn"mod.rs:206check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:55check_fn_body failedfns.rs:62args
rule "expr fn body"fns.rs:90borrow_check failednll.rs:127args
rule "borrow_check"nll.rs:138borrow_check_block failednll.rs:145rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "exists"nll.rs:300borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "loop"nll.rs:247borrow_check_loop failednll.rs:575args
rule "fixed-point"nll.rs:595borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "break"nll.rs:258drop_places failednll.rs:775args
rule "drop_places"nll.rs:789access_permitted_by_loans failednll.rs:820args
rule "access_permitted_by_loans"nll.rs:833access_permitted_by_loan failednll.rs:840args
rule "borrow of disjoint places"nll.rs:855 (failed: if_false)rule "loan is dead"nll.rs:902loan_not_required_by_live_places failednll.rs:1226args
rule "loan_not_required_by_live_places"nll.rs:1251loan_not_required_by_live_place failednll.rs:1258args
rule "loan is not required by type"nll.rs:1278loan_not_required_by_parameter failednll.rs:1326args
rule "alias-ty RFC 1214"nll.rs:1362loan_not_required_by_parameters failednll.rs:1463args
rule "loan_not_required_by_parameters"nll.rs:1484loan_not_required_by_parameter failednll.rs:1326args
rule "rigid-ty"nll.rs:1346loan_not_required_by_parameters failednll.rs:1463args
rule "loan_not_required_by_parameters"nll.rs:1484loan_not_required_by_parameter failednll.rs:1326args
rule "lifetime"nll.rs:1436loan_cannot_outlive failednll.rs:1443args
rule "loan_cannot_outlive"nll.rs:1456 (failed: if_false)
rule "write-indirect"nll.rs:882 (failed: if_let)
rule "loop"nll.rs:587borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "break"nll.rs:258drop_places failednll.rs:775args
rule "drop_places"nll.rs:789access_permitted_by_loans failednll.rs:820args
rule "access_permitted_by_loans"nll.rs:833access_permitted_by_loan failednll.rs:840args
rule "borrow of disjoint places"nll.rs:855 (failed: if_false)rule "loan is dead"nll.rs:902loan_not_required_by_live_places failednll.rs:1226args
rule "loan_not_required_by_live_places"nll.rs:1251loan_not_required_by_live_place failednll.rs:1258args
rule "loan is not required by type"nll.rs:1278loan_not_required_by_parameter failednll.rs:1326args
rule "alias-ty RFC 1214"nll.rs:1362loan_not_required_by_parameters failednll.rs:1463args
rule "loan_not_required_by_parameters"nll.rs:1484loan_not_required_by_parameter failednll.rs:1326args
rule "rigid-ty"nll.rs:1346loan_not_required_by_parameters failednll.rs:1463args
rule "loan_not_required_by_parameters"nll.rs:1484loan_not_required_by_parameter failednll.rs:1326args
rule "lifetime"nll.rs:1436loan_cannot_outlive failednll.rs:1443args
rule "loan_cannot_outlive"nll.rs:1456 (failed: if_false)
rule "write-indirect"nll.rs:882 (failed: if_let)