Negative coverage: loan_not_required_by_parameter / universal-variable / premise loan_cannot_outlive_universal_regions(env, assumptions, outlives, &loan) => ()
Premise at line 1420. Observed failure causes: failed_judgment.
universal-variable| Line | Coverage | Source |
|---|---|---|
| 1420 | 5 | (loan_cannot_outlive_universal_regions(env, assumptions, outlives, &loan) => ()) |
| ──────── ("universal-variable") | ||
| 1422 | ✗ | (loan_not_required_by_parameter(env, assumptions, outlives, loan, Variable::UniversalVar(_v)) => ()) |
5 tests failed proving this premise:
Source location: tests/borrowck.rs:2158 (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: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 "universal-variable"nll.rs:1420loan_cannot_outlive_universal_regions failednll.rs:1170args
rule "loan_not_required_by_universal_regions"nll.rs:1197 (failed: if_false)
Source location: tests/borrowck.rs:2960 (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: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 "universal-variable"nll.rs:1420loan_cannot_outlive_universal_regions failednll.rs:1170args
rule "loan_not_required_by_universal_regions"nll.rs:1197 (failed: if_false)
Source location: tests/borrowck.rs:3387 (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: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 "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 "universal-variable"nll.rs:1420loan_cannot_outlive_universal_regions failednll.rs:1170args
rule "loan_not_required_by_universal_regions"nll.rs:1197 (failed: if_false)
Source location: tests/borrowck.rs:4233 (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: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 "loop"nll.rs:247borrow_check_loop failednll.rs:575args
rule "loop"nll.rs:589borrow_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 "let"nll.rs:194borrow_check_expr_has_ty failednll.rs:351rule "block"nll.rs:364borrow_check_expr failednll.rs:372rule "call"nll.rs:443borrow_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 "universal-variable"nll.rs:1420loan_cannot_outlive_universal_regions failednll.rs:1170args
rule "loan_not_required_by_universal_regions"nll.rs:1197 (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 "let"nll.rs:194borrow_check_expr_has_ty failednll.rs:351rule "block"nll.rs:364borrow_check_expr failednll.rs:372rule "call"nll.rs:443borrow_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 "universal-variable"nll.rs:1420loan_cannot_outlive_universal_regions failednll.rs:1170args
rule "loan_not_required_by_universal_regions"nll.rs:1197 (failed: if_false)
Source location: tests/borrowck.rs:4356 (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: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 "loop"nll.rs:247borrow_check_loop failednll.rs:575args
rule "loop"nll.rs:589borrow_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 "let"nll.rs:194borrow_check_expr_has_ty failednll.rs:351rule "block"nll.rs:364borrow_check_expr failednll.rs:372rule "call"nll.rs:443borrow_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 "universal-variable"nll.rs:1420loan_cannot_outlive_universal_regions failednll.rs:1170args
rule "loan_not_required_by_universal_regions"nll.rs:1197 (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 "let"nll.rs:194borrow_check_expr_has_ty failednll.rs:351rule "block"nll.rs:364borrow_check_expr failednll.rs:372rule "call"nll.rs:443borrow_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 "universal-variable"nll.rs:1420loan_cannot_outlive_universal_regions failednll.rs:1170args
rule "loan_not_required_by_universal_regions"nll.rs:1197 (failed: if_false)