Negative coverage: borrow_check_statement / exists / premise borrow_check_block(env, assumptions_body, state, block, places_live_on_exit) => state
Premise at line 311. Observed failure causes: failed_judgment.
exists| Line | Coverage | Source |
|---|---|---|
| 307 | ✗ | (if feature_gate_enabled_in_program(&env.program, &FeatureGateName::PoloniusAlpha)) |
| 309 | N/A | (let (env, subst, block) = env.instantiate_existentially(binder)) |
| 310 | N/A | (let assumptions_body = (assumptions, wf_assumptions_for_existential_subst(&subst))) |
| 311 | 3 | (borrow_check_block(env, assumptions_body, state, block, places_live_on_exit) => state) |
| 315 | 1 | (verify_universal_outlives(env, assumptions_body, &state.all_outlives) => ()) |
| 316 | N/A | (let state = state.pop_subst(&env.env, subst)) |
| ──────── ("exists") | ||
| 318 | 54 | (borrow_check_statement(env, assumptions, state, Stmt::Exists { binder }, places_live_on_exit) => (env, state)) |
3 tests failed proving this premise:
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();
}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:311borrow_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:372rule "assign"nll.rs:404access_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 "borrow of disjoint places"nll.rs:855 (failed: if_false)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)
rule "write-indirect"nll.rs:882 (failed: if_let)rule "write-indirect"nll.rs:884 (failed: if_false)
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();
}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:311borrow_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:596 (failed: if_false)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 "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 "borrow of disjoint places"nll.rs:855 (failed: if_false)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)
rule "write-indirect"nll.rs:882 (failed: if_let)rule "write-indirect"nll.rs:884 (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 "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 "borrow of disjoint places"nll.rs:855 (failed: if_false)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)
rule "write-indirect"nll.rs:882 (failed: if_let)rule "write-indirect"nll.rs:884 (failed: if_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 } }"#]]);
}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:311borrow_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 "call"nll.rs:445verify_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 "assumption - relation"prove_wc.rs:54prove_via failedprove_via.rs:8args
rule "outlives"prove_wc.rs:152prove_outlives failedprove_outlives.rs:8args