Negative coverage: borrow_check_statement / if / premise borrow_check_block(env, assumptions, state, &else_block.block, places_live_on_exit) => else_state
Premise at line 223. Observed failure causes: failed_judgment.
if| Line | Coverage | Source |
|---|---|---|
| 212 | ✗ | (borrow_check_expr_has_ty( env, assumptions, state, condition, Ty::bool(), Either(then_block, &else_block.block).live_before(env, &state, places_live_on_exit), ) => state) |
| 222 | 2 | (borrow_check_block(env, assumptions, state, then_block, places_live_on_exit) => then_state) |
| 223 | 4 | (borrow_check_block(env, assumptions, state, &else_block.block, places_live_on_exit) => else_state) |
| 226 | N/A | (let state: FlowState = Union((then_state, else_state)).upcast()) |
| ──────── ("if") | ||
| 228 | 29 | (borrow_check_statement(env, assumptions, state, Stmt::If { condition, then_block, else_block }, places_live_on_exit) => (env, state)) |
4 tests failed proving this premise:
Source location: src/test_util.rs:516 (all coverage from this test)
#[test]
fn rustc_expectation_is_independent_of_borrowck_modes() {
let before = rustc_runs();
FormalityTest::new(NLL_ONLY_ERROR)
.rustc_err(expect_test::expect![[r#"
error[E0499]: cannot borrow `*m` as mutable more than once at a time
--> lib.rs
|
3 | pub fn foo<'a00>(mut m: &'a00 mut Map) -> &'a00 mut Map {
| ---- lifetime `'a00` defined here
4 | {
5 | let mut n: &'_ mut Map = &mut *m;
| ------- first mutable borrow occurs here
6 | if false {
7 | return n;
| - returning this value requires that `*m` is borrowed for `'a00`
8 | } else {
9 | let mut o: &'_ mut Map = &mut *m;
| ^^^^^^^ second mutable borrow occurs here
For more information about this error, try `rustc --explain E0499`.
error: could not compile `Foo` (lib) due to 1 previous error
"#]])
.borrowck_err(BorrowCheckFailure::Nll, expect_test::expect![[r#"
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
&access.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {!lt_1, ?lt_2, ?lt_3}
&lifetime.upcast() = !lt_1
the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
{
Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
{
Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
Lt::Variable(Variable::ExistentialVar(_)) => true,
Lt::Variable(Variable::BoundVar(_)) =>
panic!("cannot outlive a bound var"), Lt::Erased => true,
}, Parameter::Const(_) => panic!("cannot outlive a constant"),
})`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `m`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
place_loaned_ref = m : &!lt_1 mut Map"#]]);
assert_eq!(rustc_runs() - before, 1);
}
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "free fn"mod.rs:207check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:54check_fn_body failedfns.rs:61args
rule "expr fn body"fns.rs:89borrow_check failednll.rs:124args
rule "borrow_check"nll.rs:135borrow_check_block failednll.rs:142rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "exists"nll.rs:330borrow_check_block failednll.rs:142args
rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "if"nll.rs:223borrow_check_block failednll.rs:142args
rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "let"nll.rs:189borrow_check_expr_has_ty failednll.rs:350rule "block"nll.rs:363borrow_check_expr failednll.rs:371rule "ref"nll.rs:521access_permitted failednll.rs:862rule "access_permitted"nll.rs:878access_permitted_by_loans failednll.rs:885rule "access_permitted_by_loans"nll.rs:898access_permitted_by_loan failednll.rs:905args
rule "borrow of disjoint places"nll.rs:920 (failed: if_false)rule "loan is dead"nll.rs:967loan_not_required_by_live_places failednll.rs:1296rule "loan_not_required_by_live_places"nll.rs:1321loan_not_required_by_live_place failednll.rs:1328args
rule "loan is not required by type"nll.rs:1348loan_not_required_by_parameter failednll.rs:1396args
rule "rigid-ty"nll.rs:1416loan_not_required_by_parameters failednll.rs:1533args
rule "loan_not_required_by_parameters"nll.rs:1554loan_not_required_by_parameter failednll.rs:1396args
rule "lifetime"nll.rs:1506loan_cannot_outlive failednll.rs:1513args
rule "loan_cannot_outlive"nll.rs:1526 (failed: if_false)
rule "universal-variable"nll.rs:1490loan_cannot_outlive_universal_regions failednll.rs:1240args
rule "loan_not_required_by_universal_regions"nll.rs:1267 (failed: if_false)
rule "write-indirect"nll.rs:947 (failed: if_let)rule "write-indirect"nll.rs:949 (failed: if_false)
Source location: tests/borrowck.rs:2470 (all coverage from this test)
fn min_problem_case_3<'a>(m: &'a mut Map) -> &'a mut Map {
exists<'r0, 'r1> {
let n: &'r0 mut Map = &'r0 mut *m;
if true {
return n;
} else {
let o: &'r1 mut Map = &'r1 mut *m;
return o;
}
}
}
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "free fn"mod.rs:207check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:54check_fn_body failedfns.rs:61args
rule "expr fn body"fns.rs:89borrow_check failednll.rs:124args
rule "borrow_check"nll.rs:135borrow_check_block failednll.rs:142rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "exists"nll.rs:330borrow_check_block failednll.rs:142args
rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "if"nll.rs:223borrow_check_block failednll.rs:142args
rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "let"nll.rs:189borrow_check_expr_has_ty failednll.rs:350rule "block"nll.rs:363borrow_check_expr failednll.rs:371rule "ref"nll.rs:521access_permitted failednll.rs:862rule "access_permitted"nll.rs:878access_permitted_by_loans failednll.rs:885rule "access_permitted_by_loans"nll.rs:898access_permitted_by_loan failednll.rs:905args
rule "borrow of disjoint places"nll.rs:920 (failed: if_false)rule "loan is dead"nll.rs:967loan_not_required_by_live_places failednll.rs:1296rule "loan_not_required_by_live_places"nll.rs:1321loan_not_required_by_live_place failednll.rs:1328args
rule "loan is not required by type"nll.rs:1348loan_not_required_by_parameter failednll.rs:1396args
rule "rigid-ty"nll.rs:1416loan_not_required_by_parameters failednll.rs:1533args
rule "loan_not_required_by_parameters"nll.rs:1554loan_not_required_by_parameter failednll.rs:1396args
rule "lifetime"nll.rs:1506loan_cannot_outlive failednll.rs:1513args
rule "loan_cannot_outlive"nll.rs:1526 (failed: if_false)
rule "universal-variable"nll.rs:1490loan_cannot_outlive_universal_regions failednll.rs:1240args
rule "loan_not_required_by_universal_regions"nll.rs:1267 (failed: if_false)
rule "write-indirect"nll.rs:947 (failed: if_let)rule "write-indirect"nll.rs:949 (failed: if_false)
Source location: tests/borrowck.rs:3288 (all coverage from this test)
fn foo<'a>(m: &'a mut Map) -> &'a mut Map {
exists<'r0, 'r1> {
let n: &'r0 mut Map = &'r0 mut *m;
if false {
return n;
} else {
let o: &'r1 mut Map = &'r1 mut *m;
return o;
}
}
}
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "free fn"mod.rs:207check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:54check_fn_body failedfns.rs:61args
rule "expr fn body"fns.rs:89borrow_check failednll.rs:124args
rule "borrow_check"nll.rs:135borrow_check_block failednll.rs:142rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "exists"nll.rs:330borrow_check_block failednll.rs:142args
rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "if"nll.rs:223borrow_check_block failednll.rs:142args
rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "let"nll.rs:189borrow_check_expr_has_ty failednll.rs:350rule "block"nll.rs:363borrow_check_expr failednll.rs:371rule "ref"nll.rs:521access_permitted failednll.rs:862rule "access_permitted"nll.rs:878access_permitted_by_loans failednll.rs:885rule "access_permitted_by_loans"nll.rs:898access_permitted_by_loan failednll.rs:905args
rule "borrow of disjoint places"nll.rs:920 (failed: if_false)rule "loan is dead"nll.rs:967loan_not_required_by_live_places failednll.rs:1296rule "loan_not_required_by_live_places"nll.rs:1321loan_not_required_by_live_place failednll.rs:1328args
rule "loan is not required by type"nll.rs:1348loan_not_required_by_parameter failednll.rs:1396args
rule "rigid-ty"nll.rs:1416loan_not_required_by_parameters failednll.rs:1533args
rule "loan_not_required_by_parameters"nll.rs:1554loan_not_required_by_parameter failednll.rs:1396args
rule "lifetime"nll.rs:1506loan_cannot_outlive failednll.rs:1513args
rule "loan_cannot_outlive"nll.rs:1526 (failed: if_false)
rule "universal-variable"nll.rs:1490loan_cannot_outlive_universal_regions failednll.rs:1240args
rule "loan_not_required_by_universal_regions"nll.rs:1267 (failed: if_false)
rule "write-indirect"nll.rs:947 (failed: if_let)rule "write-indirect"nll.rs:949 (failed: if_false)
Source location: tests/mir_typeck.rs:168 (all coverage from this test)
fn foo (b: bool) -> u32 {
if b {
return 1_u32;
} else {
return false;
}
}
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "free fn"mod.rs:207check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:54check_fn_body failedfns.rs:61args
rule "expr fn body"fns.rs:89borrow_check failednll.rs:124args
rule "borrow_check"nll.rs:135borrow_check_block failednll.rs:142rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "if"nll.rs:223borrow_check_block failednll.rs:142args
rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "return"nll.rs:284prove_assignable failednll.rs:1132args
rule "subtype"nll.rs:1150prove failedfunction.rs:250args
rulefunction.rs:250prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "subtype"prove_predicate.rs:121prove_sub failedprove_sub.rs:12args
rule "normalize-l"prove_sub.rs:27prove_normalize failedprove_normalize.rs:22args
rule "normalize-r"prove_sub.rs:34prove_normalize failedprove_normalize.rs:22args
rule "if"nll.rs:223borrow_check_block failednll.rs:142args
rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "return"nll.rs:284prove_assignable failednll.rs:1132args
rule "subtype"nll.rs:1150prove failedfunction.rs:250args
rulefunction.rs:250prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "subtype"prove_predicate.rs:121prove_sub failedprove_sub.rs:12args
rule "normalize-l"prove_sub.rs:27prove_normalize failedprove_normalize.rs:22args
rule "normalize-r"prove_sub.rs:34prove_normalize failedprove_normalize.rs:22args