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, &else_block.block, places_live_on_exit) => else_state

Premise at line 221. Observed failure causes: failed_judgment.

if
LineCoverageSource
210✗(borrow_check_expr_has_ty(
env,
assumptions,
state,
condition,
Ty::bool(),
Either(then_block, &else_block.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.block, places_live_on_exit) => else_state)
224N/A(let state: FlowState = Union((then_state, else_state)).upcast())
──────── ("if")
22628(borrow_check_statement(env, assumptions, state, Stmt::If { condition, then_block, else_block }, places_live_on_exit) => (env, state))

3 tests failed proving this premise:

Source location: tests/borrowck.rs:2158 (all coverage from this test)

fn min_problem_case_3<'a>(m: &'a mut Map) -> &'a mut Map {
    exists<'r0, 'r1> {
        let n: &'r0 mut Map = &'r0 mut *m;
        if true {
            return n;
        } else {
            let o: &'r1 mut Map = &'r1 mut *m;
            return o;
        }
    }
}
Failed proof tree

Source location: tests/borrowck.rs:2960 (all coverage from this test)

fn foo<'a>(m: &'a mut Map) -> &'a mut Map {
    exists<'r0, 'r1> {
        let n: &'r0 mut Map = &'r0 mut *m;
        if false {
            return n;
        } else {
            let o: &'r1 mut Map = &'r1 mut *m;
            return o;
        }
    }
}
Failed proof tree

Source location: tests/mir_typeck.rs:168 (all coverage from this test)

fn foo (b: bool) -> u32 {
    if b {
        return 1_u32;
    } else {
        return false;
    }
}
Failed proof tree