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

Premise at line 168. Observed failure causes: failed_judgment.

basic block
LineCoverageSource
157✗(let state = state.push_scope(&env.env, label, places_live_on_exit)?)
158✗(for_all(i in 0..stmts.len()) with(env, state)
(borrow_check_statement(
env,
assumptions,
state,
&stmts[i],
stmts[i+1..].live_before(env, &state, places_live_on_exit),
) => (env, state)))
167N/A(let locals_to_drop = state.locals_dropped_in_innermost_scope())
1682(drop_places(env, assumptions, state, locals_to_drop, places_live_on_exit) => state)
169N/A(let state = state.pop_scope(label))
──────── ("basic block")
17175(borrow_check_block(env, assumptions, state, Block { label, stmts }, places_live_on_exit) => state)

2 tests failed proving this premise:

Source location: tests/borrowck.rs:1997

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

Source location: tests/borrowck.rs:2069

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