Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Negative coverage: borrow_check_statement / if / premise borrow_check_block(env, assumptions, state, then_block, places_live_on_exit) => then_state

Premise at line 220. Observed failure causes: failed_judgment.

if
LineCoverageSource
210✗(borrow_check_expr_has_ty(
env,
assumptions,
state,
condition,
Ty::bool(),
Either(then_block, else_block).live_before(env, &state, places_live_on_exit),
) => state)
2202(borrow_check_block(env, assumptions, state, then_block, places_live_on_exit) => then_state)
2213(borrow_check_block(env, assumptions, state, else_block, places_live_on_exit) => else_state)
224N/A(let state: FlowState = Union((then_state, else_state)).upcast())
──────── ("if")
22645(borrow_check_statement(env, assumptions, state, Stmt::If { condition, then_block, else_block }, places_live_on_exit) => (env, state))

2 tests failed proving this premise:

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

Source location: tests/borrowck.rs:4596

#[test]
fn flow_sensitive_invariance_use_it() {
    // [nll]: rustc errors
    FormalityTest::new(feature_gate_program(
        NLL_GATE,
        FLOW_SENSITIVE_INVARIANCE_USE_IT,
    ))
    .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 } }"#]]);

    // [polonius]: rustc errors
    FormalityTest::new(feature_gate_program(
        POLONIUS_ALPHA_GATE,
        FLOW_SENSITIVE_INVARIANCE_USE_IT,
    ))
    .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 } }"#]]);

    // [legacy]: rustc passes
    FormalityTest::new(feature_gate_program(
        POLONIUS_UNLOCKED_GATE,
        FLOW_SENSITIVE_INVARIANCE_USE_IT,
    ))
    .skip_execute()
    .ok();
}
Failed proof tree