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 / exists / premise borrow_check_block(env, assumptions_body, state, block, places_live_on_exit) => state

Premise at line 300. Observed failure causes: failed_judgment.

exists
LineCoverageSource
296✗(if feature_gate_enabled_in_program(&env.program, &FeatureGateName::PoloniusUnlocked))
298N/A(let (env, subst, block) = env.instantiate_existentially(binder))
299N/A(let assumptions_body = (assumptions, wf_assumptions_for_existential_subst(&subst)))
3001(borrow_check_block(env, assumptions_body, state, block, places_live_on_exit) => state)
301N/A(let state = state.pop_subst(&env.env, subst))
──────── ("exists")
30354(borrow_check_statement(env, assumptions, state, Stmt::Exists { binder }, places_live_on_exit) => (env, state))

1 test failed proving this premise:

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 } }"#]]);
}
Failed proof tree