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	23	(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	36	(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:4472 (all coverage from this test)

fn use_it<'a, 'b>() -> u32 {
    exists<'r0> {
        let v: Invariant<'r0> = create_invariant::<'r0>();
        if true {
            return sink::<'a, 'r0>(v);
        } else {
            return sink::<'b, 'r0>(v);
        }
    }
}

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" prove_wc.rs:48
    
    prove_via failed prove_via.rs:8
    
    args
    
    rule "outlives" prove_wc.rs:146
    
    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) => ()`