Negative coverage: borrow_check_statement / expr / premise borrow_check_expr( env, assumptions, state, expr, places_live_on_exit ) => (_init_ty, state)
Premise at line 230. Observed failure causes: failed_judgment.
expr| Line | Coverage | Source |
|---|---|---|
| 230 | 18 | (borrow_check_expr( env, assumptions, state, expr, places_live_on_exit ) => (_init_ty, state)) |
| ──────── ("expr") | ||
| 238 | 36 | (borrow_check_statement(env, assumptions, state, Stmt::Expr { expr }, places_live_on_exit) => (env, state)) |
18 tests failed proving this premise:
Source location: tests/borrowck.rs:227
fn foo() -> u32 {
let x: Pair;
x.first = 1_u32;
return 0_u32;
}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 "expr"nll.rs:230borrow_check_expr failednll.rs:372args
rule "assign"nll.rs:404access_permitted failednll.rs:797args
rule "access_permitted"nll.rs:809 (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 "borrow of disjoint places"nll.rs:855 (failed: if_false)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 "write-indirect"nll.rs:882 (failed: if_let)
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 "borrow of disjoint places"nll.rs:855 (failed: if_false)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 "write-indirect"nll.rs:882 (failed: if_let)
Source location: tests/borrowck.rs:2256
fn foo<'a, 'b>(v1: &'a u32, v2: &'b u32) -> () {
let output: &'b u32 = v2;
loop {
output = v1;
}
}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 "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 "expr"nll.rs:230borrow_check_expr failednll.rs:372args
rule "assign"nll.rs:402prove_assignable failednll.rs:1067args
rule "subtype"nll.rs:1085verify_universal_outlives failedoutlives.rs:8args
rule "verify_universal_outlives"outlives.rs:20only_assumed_outlives failedoutlives.rs:27args
rule "universal lifetime"outlives.rs:49can_outlive failedoutlives.rs:56args
rule "universal target"outlives.rs:81prove failedoutlives.rs:81args
ruleoutlives.rs:81prove_wc_list failedprove_wc_list.rs:8args
rule "some"prove_wc_list.rs:26prove_wc failedprove_wc.rs:21args
rule "outlives"prove_wc.rs:152prove_outlives failedprove_outlives.rs:8args
rule "assign"nll.rs:402prove_assignable failednll.rs:1067args
rule "subtype"nll.rs:1085verify_universal_outlives failedoutlives.rs:8args
rule "verify_universal_outlives"outlives.rs:20only_assumed_outlives failedoutlives.rs:27args
rule "universal lifetime"outlives.rs:49can_outlive failedoutlives.rs:56args
rule "universal target"outlives.rs:81prove failedoutlives.rs:81args
ruleoutlives.rs:81prove_wc_list failedprove_wc_list.rs:8args
rule "some"prove_wc_list.rs:26prove_wc failedprove_wc.rs:21args
rule "outlives"prove_wc.rs:152prove_outlives failedprove_outlives.rs:8args
rule "loop"nll.rs:587borrow_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:402prove_assignable failednll.rs:1067args
rule "subtype"nll.rs:1085verify_universal_outlives failedoutlives.rs:8args
rule "verify_universal_outlives"outlives.rs:20only_assumed_outlives failedoutlives.rs:27args
rule "universal lifetime"outlives.rs:49can_outlive failedoutlives.rs:56args
rule "universal target"outlives.rs:81prove failedoutlives.rs:81args
ruleoutlives.rs:81prove_wc_list failedprove_wc_list.rs:8args
rule "some"prove_wc_list.rs:26prove_wc failedprove_wc.rs:21args
rule "outlives"prove_wc.rs:152prove_outlives failedprove_outlives.rs:8args
rule "assign"nll.rs:402prove_assignable failednll.rs:1067args
rule "subtype"nll.rs:1085verify_universal_outlives failedoutlives.rs:8args
rule "verify_universal_outlives"outlives.rs:20only_assumed_outlives failedoutlives.rs:27args
rule "universal lifetime"outlives.rs:49can_outlive failedoutlives.rs:56args
rule "universal target"outlives.rs:81prove failedoutlives.rs:81args
ruleoutlives.rs:81prove_wc_list failedprove_wc_list.rs:8args
rule "some"prove_wc_list.rs:26prove_wc failedprove_wc.rs:21args
rule "outlives"prove_wc.rs:152prove_outlives failedprove_outlives.rs:8args
Source location: tests/borrowck.rs:2541
fn foo() -> i32 {
exists<'r0, 'r1> {
let x: i32 = 0_i32;
let r: &'r0 i32;
'a: loop {
r; // this *may* read from `y` in a previous iteration
let y: i32 = 0_i32;
r = &'r1 y;
continue 'a;
}
}
}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 "expr"nll.rs:230borrow_check_expr failednll.rs:372args
rule "place"nll.rs:504access_permitted failednll.rs:797args
rule "access_permitted"nll.rs:809 (failed: if_false)
rule "place"nll.rs:504access_permitted failednll.rs:797args
rule "access_permitted"nll.rs:809 (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 "expr"nll.rs:230borrow_check_expr failednll.rs:372args
rule "place"nll.rs:504access_permitted failednll.rs:797args
rule "access_permitted"nll.rs:809 (failed: if_false)
rule "place"nll.rs:504access_permitted failednll.rs:797args
rule "access_permitted"nll.rs:809 (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 "borrow of disjoint places"nll.rs:855 (failed: if_false)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 "write-indirect"nll.rs:882 (failed: if_let)
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 "borrow of disjoint places"nll.rs:855 (failed: if_false)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 "write-indirect"nll.rs:882 (failed: if_let)
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;
}
}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 "borrow of disjoint places"nll.rs:855 (failed: if_false)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 "write-indirect"nll.rs:882 (failed: if_let)
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;
}
}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 "borrow of disjoint places"nll.rs:855 (failed: if_false)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 "write-indirect"nll.rs:882 (failed: if_let)rule "write-indirect"nll.rs:882 (failed: if_let)
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);
}
}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 "borrow of disjoint places"nll.rs:855 (failed: if_false)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 "write-indirect"nll.rs:882 (failed: if_let)
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;
}
}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 "borrow of disjoint places"nll.rs:855 (failed: if_false)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 "write-indirect"nll.rs:882 (failed: if_let)
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;
}
}Proof trees omitted for the remaining 8 tests.
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:4651
#[test]
fn flow_sensitive_invariance_use_both() {
FormalityTest::new(feature_gate_program(
NLL_GATE,
FLOW_SENSITIVE_INVARIANCE_USE_BOTH,
))
.skip_execute()
.err(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
FLOW_SENSITIVE_INVARIANCE_USE_BOTH,
))
.skip_execute()
.err(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
FLOW_SENSITIVE_INVARIANCE_USE_BOTH,
))
.skip_execute()
.err(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
}Source location: tests/borrowck.rs:4661
#[test]
fn flow_sensitive_invariance_use_both() {
FormalityTest::new(feature_gate_program(
NLL_GATE,
FLOW_SENSITIVE_INVARIANCE_USE_BOTH,
))
.skip_execute()
.err(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
FLOW_SENSITIVE_INVARIANCE_USE_BOTH,
))
.skip_execute()
.err(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
FLOW_SENSITIVE_INVARIANCE_USE_BOTH,
))
.skip_execute()
.err(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
}Source location: tests/borrowck.rs:4671
#[test]
fn flow_sensitive_invariance_use_both() {
FormalityTest::new(feature_gate_program(
NLL_GATE,
FLOW_SENSITIVE_INVARIANCE_USE_BOTH,
))
.skip_execute()
.err(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
FLOW_SENSITIVE_INVARIANCE_USE_BOTH,
))
.skip_execute()
.err(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
FLOW_SENSITIVE_INVARIANCE_USE_BOTH,
))
.skip_execute()
.err(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
}Source location: tests/mir_typeck.rs:595
fn foo (v1: u32) -> u32 {
let v2: Dummy = Dummy { value: 1_u32 };
v2.nonexistent = 2_u32;
return v1;
}Source location: tests/mir_typeck.rs:613
fn foo (v1: u32) -> u32 {
let v2: Dummy = Dummy { value: 1_u32 };
v1.value = 2_u32;
return v1;
}