Negative coverage: borrow_check_expr / ref / premise access_permitted( env, assumptions, state, Access::new(access_kind, place), places_live_on_exit, ) => state
Premise at line 521. Observed failure causes: failed_judgment.
ref| Line | Coverage | Source |
|---|---|---|
| 509 | ✗ | (borrow_check_place_expr( env, assumptions, state, place, ) => (place, state)) |
| 517 | N/A | (let access_kind = match kind { RefKind::Shared => AccessKind::Read, RefKind::Mut => AccessKind::Write, }) |
| 521 | 8 | (access_permitted( env, assumptions, state, Access::new(access_kind, place), places_live_on_exit, ) => state) |
| 530 | N/A | (let state = state.with_loan(Loan::new(lt, place, kind))) |
| 531 | N/A | (let state = state.with_outlives(&reborrow_constraints(place, lt))) |
| 538 | 1 | (verify_universal_outlives(env, assumptions, &state.current.outlives) => ()) |
| 539 | N/A | (let ty = place.ty.ref_ty_of_kind(kind, lt)) |
| ──────── ("ref") | ||
| 541 | 41 | (borrow_check_expr(env, assumptions, state, Expr::Ref { kind, lt, place }, places_live_on_exit) => (ty, state)) |
8 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/borrowck.rs:3536 (all coverage from this test)
fn bar() -> u32 {
exists<'r0, 'r1, 'r2> {
let v: u32 = 0_u32;
let p: &'r0 u32 = &'r1 v;
let _: u32 = foo::<'r2>(&'r2 mut v);
return *p;
}
}
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:302borrow_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:350args
rule "block"nll.rs:363borrow_check_expr failednll.rs:371args
rule "call"nll.rs:478borrow_check_expr_has_ty failednll.rs:350args
rule "block"nll.rs:363borrow_check_expr failednll.rs:371args
rule "ref"nll.rs:521access_permitted failednll.rs:862args
rule "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:1296args
rule "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 "alias-ty RFC 1214"nll.rs:1432loan_not_required_by_parameters failednll.rs:1533args
rule "loan_not_required_by_parameters"nll.rs:1554loan_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 "write-indirect"nll.rs:947 (failed: if_let)
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 "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:4326 (all coverage from this test)
fn conditional() -> u32 {
exists<'r0, 'r1, 'r2, 'r3> {
let b: X = X { value: 0_u32 };
let p: &'r0 mut X = &'r1 mut b;
'l: loop {
let now: &'r2 mut X = &'r2 mut *p;
if true {
if true {
let next: &'r3 mut X = next_of::<'r3>(&'r3 mut *now);
p = next;
} else {
}
} else {
break 'l;
}
}
return 0_u32;
}
}
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:312borrow_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 "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 "write-indirect"nll.rs:947 (failed: if_let)rule "write-indirect"nll.rs:949 (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 "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 "write-indirect"nll.rs:947 (failed: if_let)rule "write-indirect"nll.rs:949 (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 "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:947 (failed: if_let)rule "write-indirect"nll.rs:949 (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 "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:947 (failed: if_let)rule "write-indirect"nll.rs:949 (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 "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:947 (failed: if_let)rule "write-indirect"nll.rs:949 (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 "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:947 (failed: if_let)rule "write-indirect"nll.rs:949 (failed: if_false)