Negative coverage: loan_cannot_outlive_universal_regions / loan_not_required_by_universal_regions / premise if outlived_by_loan.iter().all(\|p\| match p { // If ’0: Tthen’0must hold for entire fn body... Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() { // If’0: ’staticthen’0must hold for entire fn body... Lt::Static => false, // If’0: ’afor some lifetime parameter’a, then ’0must hold for entire fn body... Lt::Variable(Variable::UniversalVar(_)) => false, // If’0: ’1, that's fine. Lt::Variable(Variable::ExistentialVar(_)) => true, Lt::Variable(Variable::BoundVar(_)) => panic!("cannot outlive a bound var"), // Erased lifetimes are used in codegen; treat like existential. Lt::Erased => true, }, // Not really clear what this would mean Parameter::Const(_) => panic!("cannot outlive a constant"), })
Premise at line 1267. Observed failure causes: if_false.
loan_not_required_by_universal_regions| Line | Coverage | Source |
|---|---|---|
| 1266 | N/A | (let outlived_by_loan = transitively_outlived_by(&env, &outlives, &loan.lt)) |
| 1267 | 6 | (if outlived_by_loan.iter().all(|p| match p { // If `'0: T` then `'0` must hold for entire fn body... Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref() { // If `'0: 'static` then `'0` must hold for entire fn body... Lt::Static => false, // If `'0: 'a` for some lifetime parameter `'a`, then `'0` must hold for entire fn body... Lt::Variable(Variable::UniversalVar(_)) => false, // If `'0: '1`, that's fine. Lt::Variable(Variable::ExistentialVar(_)) => true, Lt::Variable(Variable::BoundVar(_)) => panic!("cannot outlive a bound var"), // Erased lifetimes are used in codegen; treat like existential. Lt::Erased => true, }, // Not really clear what this would mean Parameter::Const(_) => panic!("cannot outlive a constant"), })) |
| ──────── ("loan_not_required_by_universal_regions") | ||
| 1291 | 18 | (loan_cannot_outlive_universal_regions(env, _assumptions, outlives, loan) => ()) |
6 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 "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 "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)
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 "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 "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)
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 "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 "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)
Source location: tests/borrowck.rs:3715 (all coverage from this test)
fn reborrow<'a>(a: &'a mut u8) -> &'a mut u8 {
exists<'r0, 'r1, 'r2, 'r3> {
// This creates an outlives constraint
let b: &'r1 mut u8 = &'r0 mut *a;
if true {
return b;
} else {
// this means the loan remains live
}
// If the outlives constraint propagated here,
// we would get an error.
let c: &'r3 mut u8 = &'r2 mut *a;
return c;
}
}
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 "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 "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 "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)
Source location: tests/borrowck.rs:4592 (all coverage from this test)
fn next<'a>(d: &'a mut Decoder) -> &'a u32 {
exists<'r0, 'r1> {
'l: loop {
let buf: &'r0 u32 = fill_buf::<'r0>(&'r0 mut (*d).buf_read);
let s: &'r1 u32 = decode::<'r1>(buf);
if true {
return s;
} else {
}
}
}
}
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 "loop"nll.rs:249borrow_check_loop failednll.rs:640args
rule "loop"nll.rs:654borrow_check_loop failednll.rs:640args
rule "fixed-point"nll.rs:660borrow_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 "call"nll.rs:478borrow_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 "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 "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 "loop"nll.rs:652borrow_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 "call"nll.rs:478borrow_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 "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 "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)
Source location: tests/borrowck.rs:4715 (all coverage from this test)
fn next<'s>(f: &'s mut Filter) -> &'s mut u32 {
exists<'r0, 'r1, 'r2> {
'l: loop {
let item: &'r0 mut u32 = iter_next::<'r0>(&'r0 mut (*f).iter);
if true {
let keep: bool = call_predicate::<'r1, 'r2>(&'r1 mut (*f).predicate, &'r2 *item);
if keep {
return item;
} else {
}
} else {
break 'l;
}
}
return no_item::<'s>();
}
}
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 "loop"nll.rs:249borrow_check_loop failednll.rs:640args
rule "loop"nll.rs:654borrow_check_loop failednll.rs:640args
rule "fixed-point"nll.rs:660borrow_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 "call"nll.rs:478borrow_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 "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 "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 "loop"nll.rs:652borrow_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 "call"nll.rs:478borrow_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 "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 "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)