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 / break / premise drop_places(env, assumptions, state, locals_to_drop, places_live_on_exit) => state

Premise at line 260. Observed failure causes: failed_judgment.

break
LineCoverageSource
258✗(if state.scope_has_label(label))
259N/A(let locals_to_drop = state.locals_dropped_to_label(label))
2602(drop_places(env, assumptions, state, locals_to_drop, places_live_on_exit) => state)
261N/A(let state = state.with_break(label))
262N/A(let state = state.diverges())
──────── ("break")
26417(borrow_check_statement(env, assumptions, state, Stmt::Break { label }, places_live_on_exit) => (env, state))

2 tests failed proving this premise:

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

fn foo() -> i32 {
    exists<'r0, 'r1> {
        let v2: &'r0 i32;
        'a: {
            let v1: i32 = 0_i32;
            v2 = &'r1 v1;
            break 'a;
        }
        return *v2;
    }
}
Failed proof tree

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

fn foo() -> i32 {
    exists<'r0, 'r1> {
        let r: &'r0 i32;
        'a: loop {
            let x: i32 = 0_i32;
            r = &'r1 x;
            break 'a;
        }
        return *r;
    }
}
Failed proof tree

How to read this page