Negative coverage: loan_cannot_outlive / loan_cannot_outlive / premise if !outlived_by_loan.contains(&lifetime.upcast())
Premise at line 1456. Observed failure causes: if_false.
loan_cannot_outlive| Line | Coverage | Source |
|---|---|---|
| 1455 | N/A | (let outlived_by_loan = transitively_outlived_by(env, outlives, &loan.lt)) |
| 1456 | 25 | (if !outlived_by_loan.contains(&lifetime.upcast())) |
| ──────── ("loan_cannot_outlive") | ||
| 1458 | 12 | (loan_cannot_outlive(env, _assumptions, outlives, loan, lifetime) => ()) |
25 tests failed proving this premise:
Source location: tests/borrowck.rs:1792
fn foo() -> Datum {
exists<'r0, 'r1> {
let x: Datum = Datum { value: 0_u32 };
let r: &'r0 Datum = &'r1 x;
let y: Datum = x;
return *r;
}
}
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:327borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "let"nll.rs:194borrow_check_expr_has_ty failednll.rs:351args
rule "block"nll.rs:364borrow_check_expr failednll.rs:372args
rule "place"nll.rs:504access_permitted failednll.rs:797args
rule "access_permitted"nll.rs:813access_permitted_by_loans failednll.rs:820rule "access_permitted_by_loans"nll.rs:833access_permitted_by_loan failednll.rs:840args
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)
Source location: tests/borrowck.rs:1901
fn foo() -> i32 {
exists<'r0, 'r1> {
let v1: i32 = 0_i32;
let v2: &'r0 mut i32 = &mut 'r1 v1;
// This should result in an error
v1 = 1_i32;
return *v2;
}
}
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:327borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "expr"nll.rs:230borrow_check_expr failednll.rs:372args
rule "assign"nll.rs:404access_permitted failednll.rs:797args
rule "access_permitted"nll.rs:813access_permitted_by_loans failednll.rs:820rule "access_permitted_by_loans"nll.rs:833access_permitted_by_loan failednll.rs:840args
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)
Source location: tests/borrowck.rs:1939
fn foo() -> i32 {
exists<'r0, 'r1> {
let v1: i32 = 0_i32;
let v2: &'r0 i32 = &'r1 v1;
v1 = 1_i32;
return *v2;
}
}
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:327borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "expr"nll.rs:230borrow_check_expr failednll.rs:372args
rule "assign"nll.rs:404access_permitted failednll.rs:797args
rule "access_permitted"nll.rs:813access_permitted_by_loans failednll.rs:820rule "access_permitted_by_loans"nll.rs:833access_permitted_by_loan failednll.rs:840args
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)
Source location: tests/borrowck.rs:1989
#[test]
fn min_problem_case_3() {
FormalityTest::new(feature_gate_program(NLL_GATE, MIN_PROBLEM_CASE_3))
.skip_execute()
.err(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"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
MIN_PROBLEM_CASE_3,
))
.skip_execute()
.ok();
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
MIN_PROBLEM_CASE_3,
))
.skip_execute()
.ok();
}
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:330borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "if"nll.rs:221borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "let"nll.rs:194borrow_check_expr_has_ty failednll.rs:351rule "block"nll.rs:364borrow_check_expr failednll.rs:372rule "ref"nll.rs:478access_permitted failednll.rs:797rule "access_permitted"nll.rs:813access_permitted_by_loans failednll.rs:820rule "access_permitted_by_loans"nll.rs:833access_permitted_by_loan failednll.rs:840args
rule "loan is dead"nll.rs:902loan_not_required_by_live_places failednll.rs:1226rule "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 "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)
Source location: tests/borrowck.rs:2061
fn foo() -> i32 {
exists<'r0, 'r1> {
let v2: &'r0 i32;
{
let v1: i32 = 0_i32;
v2 = &'r1 v1;
}
return *v2;
}
}
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:327borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "block"nll.rs:290borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:169drop_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 "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)
Source location: tests/borrowck.rs:2133
fn foo() -> i32 {
exists<'r0, 'r1> {
let v2: &'r0 mut i32;
{
let v1: i32 = 0_i32;
v2 = &mut 'r1 v1;
}
return *v2;
}
}
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:327borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "block"nll.rs:290borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:169drop_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 "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)
Source location: tests/borrowck.rs:2175
fn foo() -> i32 {
exists<'r0, 'r1> {
let v2: &'r0 i32;
'a: {
let v1: i32 = 0_i32;
v2 = &'r1 v1;
break 'a;
}
return *v2;
}
}
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:327borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "block"nll.rs:290borrow_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 "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)
Source location: tests/borrowck.rs:2494
fn foo() -> i32 {
exists<'r0, 'r1> {
let r: &'r0 i32;
'a: loop {
let y: i32 = 0_i32;
r = &'r1 y;
continue 'a;
}
r; // only an error because of false edges, assumption that all loops terminate
}
}
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:327borrow_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 "continue"nll.rs:271drop_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 "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 "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 "loop"nll.rs:587borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "continue"nll.rs:271drop_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 "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 "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)
Source location: tests/borrowck.rs:2608
fn foo() -> i32 {
exists<'r0, 'r1> {
let r: &'r0 i32;
'a: loop {
let x: i32 = 0_i32;
r = &'r1 x;
break 'a;
}
return *r;
}
}
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:327borrow_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 "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 "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 "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)
Source location: tests/borrowck.rs:2735
fn foo() -> u32 {
exists<'r0, 'r1> {
let a: u32 = 22_u32;
let p: &'r0 u32 = &'r1 a;
'l: loop {
if true {
a = 23_u32;
continue 'l;
} else {
break 'l;
}
}
return *p;
}
}
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:327borrow_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 "if"nll.rs:220borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "expr"nll.rs:230borrow_check_expr failednll.rs:372args
rule "assign"nll.rs:404access_permitted failednll.rs:797args
rule "access_permitted"nll.rs:813access_permitted_by_loans failednll.rs:820rule "access_permitted_by_loans"nll.rs:833access_permitted_by_loan failednll.rs:840args
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 "loop"nll.rs:587borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "if"nll.rs:220borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "expr"nll.rs:230borrow_check_expr failednll.rs:372args
rule "assign"nll.rs:404access_permitted failednll.rs:797args
rule "access_permitted"nll.rs:813access_permitted_by_loans failednll.rs:820rule "access_permitted_by_loans"nll.rs:833access_permitted_by_loan failednll.rs:840args
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)
Source location: tests/borrowck.rs:2798
#[test]
fn if_false_borrowck() {
FormalityTest::new(feature_gate_program(NLL_GATE, IF_FALSE_BORROWCK))
.skip_execute()
.err(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"#]]);
FormalityTest::new(feature_gate_program(POLONIUS_ALPHA_GATE, IF_FALSE_BORROWCK))
.skip_execute()
.ok();
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
IF_FALSE_BORROWCK,
))
.skip_execute()
.ok();
}
Proof trees omitted for the remaining 15 tests.
Source location: tests/borrowck.rs:2870
fn foo() -> u32 {
exists<'r0, 'r1, 'r2> {
let a: u32 = 22_u32;
let b: u32 = 22_u32;
let p: &'r0 u32 = &'r1 a;
a = 23_u32;
'l: loop {
p = &'r2 b;
break 'l;
}
return *p;
}
}
Source location: tests/borrowck.rs:3049
fn bar() -> u32 {
exists<'r0, 'r1, 'r2> {
let v: u32 = 0_u32;
let p: &'r0 u32 = &'r1 v;
let _: u32 = foo::<'r2>(&mut 'r2 v);
return *p;
}
}
Source location: tests/borrowck.rs:3097
fn foo() -> u32 {
exists<'r0, 'r1> {
let p: Point = Point { x: 0_u32, y: 0_u32 };
let b1: &'r0 mut u32 = &mut 'r1 p.x;
p.x = 1_u32;
return *b1;
}
}
Source location: tests/borrowck.rs:3131
fn foo() -> u32 {
exists<'r0, 'r1> {
let v1: u32 = 22_u32;
let v2: &'r0 mut u32 = &mut 'r1 v1;
let w: Wrapper = Wrapper { value: v1 };
return *v2;
}
}
Source location: tests/borrowck.rs:3168
fn foo() -> u32 {
exists<'r0> {
let v1: u32 = 0_u32;
let w: Wrapper<'r0> = Wrapper::<'r0> { value: &mut 'r0 v1 };
v1 = 1_u32;
return *(w.value);
}
}
Source location: tests/borrowck.rs:3230
#[test]
fn outlive_before_return_does_not_affect_merged_paths() {
FormalityTest::new(feature_gate_program(
NLL_GATE,
OUTLIVE_BEFORE_RETURN_DOES_NOT_AFFECT_MERGED_PATHS,
))
.skip_execute()
.err(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 = *(a : &!lt_1 mut u8) : <&!lt_1 mut u8 as Derefable>::Target
&access.place = *(a : &!lt_1 mut u8) : <&!lt_1 mut u8 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, ?lt_4, ?lt_5}
&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 `a`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(a : &!lt_1 mut u8) : <&!lt_1 mut u8 as Derefable>::Target
place_loaned_ref = a : &!lt_1 mut u8"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
OUTLIVE_BEFORE_RETURN_DOES_NOT_AFFECT_MERGED_PATHS,
))
.skip_execute()
.ok();
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
OUTLIVE_BEFORE_RETURN_DOES_NOT_AFFECT_MERGED_PATHS,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:3338
fn foo() -> u32 {
exists<'r0, 'r1, 'r2> {
let x: u32 = 22_u32;
let p: &'r1 u32 = &'r0 x;
let q: &'r2 u32 = p;
x = 1_u32;
q;
return 0_u32;
}
}
Source location: tests/borrowck.rs:3502
fn foo() -> u32 {
exists<'r0, 'r1> {
let x: u32 = 22_u32;
let helper: &'r1 u32 = &'r0 x;
x = 1_u32;
helper;
return 0_u32;
}
}
Source location: tests/borrowck.rs:3751
#[test]
fn issue_63908_remove_last_node_iterative() {
FormalityTest::new(feature_gate_program(
NLL_GATE,
ISSUE_63908_REMOVE_LAST_NODE_ITERATIVE,
))
.skip_execute()
.err(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 = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
&access.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List 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_2, ?lt_3}
&lifetime.upcast() = ?lt_2
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `cursor`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
place_loaned_ref = cursor : &?lt_2 mut List"#]]);
// [polonius]: rustc errors here (known-bug #63908), same as [nll].
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_63908_REMOVE_LAST_NODE_ITERATIVE,
))
.skip_execute()
.err(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 = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
&access.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List 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_2, ?lt_3}
&lifetime.upcast() = ?lt_2
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `cursor`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
place_loaned_ref = cursor : &?lt_2 mut List"#]]);
// [legacy]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_63908_REMOVE_LAST_NODE_ITERATIVE,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:3776
#[test]
fn issue_63908_remove_last_node_iterative() {
FormalityTest::new(feature_gate_program(
NLL_GATE,
ISSUE_63908_REMOVE_LAST_NODE_ITERATIVE,
))
.skip_execute()
.err(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 = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
&access.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List 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_2, ?lt_3}
&lifetime.upcast() = ?lt_2
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `cursor`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
place_loaned_ref = cursor : &?lt_2 mut List"#]]);
// [polonius]: rustc errors here (known-bug #63908), same as [nll].
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_63908_REMOVE_LAST_NODE_ITERATIVE,
))
.skip_execute()
.err(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 = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
&access.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List 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_2, ?lt_3}
&lifetime.upcast() = ?lt_2
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `cursor`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
place_loaned_ref = cursor : &?lt_2 mut List"#]]);
// [legacy]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_63908_REMOVE_LAST_NODE_ITERATIVE,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:3917
#[test]
fn issue_57165_conditional() {
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_57165_CONDITIONAL))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "fixed-point" at (nll.rs) failed because
condition evaluated to false: `state0 == state1`
state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)})
state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)})
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 = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
&access.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X 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_3, ?lt_4}
&lifetime.upcast() = ?lt_1
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `p`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
place_loaned_ref = p : &?lt_1 mut X
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 = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
&access.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X 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_3, ?lt_4}
&lifetime.upcast() = ?lt_1
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `p`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
place_loaned_ref = p : &?lt_1 mut X"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_57165_CONDITIONAL,
))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "fixed-point" at (nll.rs) failed because
condition evaluated to false: `state0 == state1`
state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)})
state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)})
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 = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
&access.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X 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_3, ?lt_4}
&lifetime.upcast() = ?lt_1
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `p`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
place_loaned_ref = p : &?lt_1 mut X
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 = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
&access.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X 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_3, ?lt_4}
&lifetime.upcast() = ?lt_1
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `p`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
place_loaned_ref = p : &?lt_1 mut X"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_57165_CONDITIONAL,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:3964
#[test]
fn issue_57165_conditional() {
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_57165_CONDITIONAL))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "fixed-point" at (nll.rs) failed because
condition evaluated to false: `state0 == state1`
state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)})
state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)})
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 = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
&access.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X 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_3, ?lt_4}
&lifetime.upcast() = ?lt_1
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `p`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
place_loaned_ref = p : &?lt_1 mut X
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 = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
&access.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X 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_3, ?lt_4}
&lifetime.upcast() = ?lt_1
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `p`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
place_loaned_ref = p : &?lt_1 mut X"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_57165_CONDITIONAL,
))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "fixed-point" at (nll.rs) failed because
condition evaluated to false: `state0 == state1`
state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)})
state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)})
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 = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
&access.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X 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_3, ?lt_4}
&lifetime.upcast() = ?lt_1
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `p`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
place_loaned_ref = p : &?lt_1 mut X
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 = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
&access.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X 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_3, ?lt_4}
&lifetime.upcast() = ?lt_1
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `p`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
place_loaned_ref = p : &?lt_1 mut X"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_57165_CONDITIONAL,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4316
#[test]
fn issue_46859_decoder_next() {
// [nll]: rustc errors
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_46859_DECODER_NEXT))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "fixed-point" at (nll.rs) failed because
condition evaluated to false: `state0 == state1`
state0 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)})
state1 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {loan(?lt_2, *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32, mut)}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)})
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 = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
&access.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
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 `*(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct]`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `d`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
place_loaned_ref = d : &!lt_1 mut Decoder
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 = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
&access.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
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 `*(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct]`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `d`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
place_loaned_ref = d : &!lt_1 mut Decoder"#]]);
// [polonius]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_46859_DECODER_NEXT,
))
.skip_execute()
.ok();
// [legacy]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_46859_DECODER_NEXT,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4458
#[test]
fn issue_92985_filtering_lending_iterator() {
// [nll]: rustc errors
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_92985_FILTER_NEXT))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "fixed-point" at (nll.rs) failed because
condition evaluated to false: `state0 == state1`
state0 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)})
state1 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut), loan(?lt_3, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . predicate[Filter , struct] : u32, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut)}, {}))}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)})
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 = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
&access.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
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, ?lt_4}
&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 `*(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct]`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `f`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
place_loaned_ref = f : &!lt_1 mut Filter
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 = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
&access.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
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, ?lt_4}
&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 `*(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct]`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `f`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
place_loaned_ref = f : &!lt_1 mut Filter"#]]);
// [polonius]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_92985_FILTER_NEXT,
))
.skip_execute()
.ok();
// [legacy]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_92985_FILTER_NEXT,
))
.skip_execute()
.ok();
}