Negative coverage: `borrow_check_statement` / `exists` / premise `verify_universal_outlives(env, assumptions_body, &state.all_outlives) => ()`

Premise at line 315. 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))

1 test failed proving this premise:

Source location: tests/borrowck.rs:4607

#[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

check_all_crates failed mod.rs:41
- args
- rule "check all prefixes" mod.rs:53
  - check_crate failed mod.rs:60
    
    args
    
    rule "check crate" mod.rs:73
    
    check_crate_item failed mod.rs:178
    
    rule "free fn" mod.rs:206
    
    check_free_fn failed fns.rs:14
    
    args
    
    rule "check free fn" fns.rs:24
    
    check_fn failed fns.rs:31
    
    args
    
    rule "check fn" fns.rs:55
    
    check_fn_body failed fns.rs:62
    
    args
    
    rule "expr fn body" fns.rs:90
    
    borrow_check failed nll.rs:127
    
    args
    
    rule "borrow_check" nll.rs:138
    
    borrow_check_block failed nll.rs:145
    
    rule "basic block" nll.rs:160
    
    borrow_check_statement failed nll.rs:177
    
    args
    
    rule "exists" nll.rs:315
    
    verify_universal_outlives failed outlives.rs:8
    
    args
    
    rule "verify_universal_outlives" outlives.rs:20
    
    only_assumed_outlives failed outlives.rs:27
    
    args
    
    rule "universal lifetime" outlives.rs:49
    
    can_outlive failed outlives.rs:56
    
    args
    
    rule "universal target" outlives.rs:81
    
    prove failed outlives.rs:81
    
    args
    
    rule outlives.rs:81
    
    prove_wc_list failed prove_wc_list.rs:8
    
    args
    
    rule "some" prove_wc_list.rs:26
    
    prove_wc failed prove_wc.rs:21
    
    args
    
    rule "assumption - relation" prove_wc.rs:54
    
    prove_via failed prove_via.rs:8
    
    args
    
    rule "outlives" prove_wc.rs:152
    
    prove_outlives failed prove_outlives.rs:8
    
    args

Keyboard shortcuts

A MIR Formality

Negative coverage: borrow_check_statement / exists / premise verify_universal_outlives(env, assumptions_body, &state.all_outlives) => ()

Negative coverage: `borrow_check_statement` / `exists` / premise `verify_universal_outlives(env, assumptions_body, &state.all_outlives) => ()`