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_expr / place / premise prove_place_is_movable(env, assumptions, state, place) => state

Premise at line 506. Observed failure causes: failed_judgment.

place
LineCoverageSource
5022(borrow_check_place_expr(env, assumptions, state, place) => (place, state))
503✗(access_kind_for_place_use(env, assumptions, state, place) => (access_kind, state))
50411(access_permitted(env, assumptions, state, Access::new(access_kind, place), places_live_on_exit) => state)
505N/A(let state = if matches!(access_kind, AccessKind::Move) { state.with_uninit(&place.to_place_expression()) } else { state.clone() })
5063(prove_place_is_movable(env, assumptions, state, place) => state)
──────── ("place")
50888(borrow_check_expr(env, assumptions, state, Expr::Place(place), places_live_on_exit) => (&place.ty, state))

3 tests failed proving this premise:

Source location: tests/borrowck.rs:473

fn foo() -> Datum {
    exists<'r0, 'r1> {
        let x: Datum = Datum { value: 0_u32 };
        let r: &'r0 Datum = &'r1 x;
        let y: Datum = *r;
        return y;
    }
}
Failed proof tree
… (200 of 1236 nodes shown)

Source location: tests/borrowck.rs:1132

fn foo() -> Datum {
    exists<'r0, 'r1> {
        let x: Datum = Datum { value: 0_u32 };
        let r: &'r0 mut Datum = &mut 'r1 x;
        let y: Datum = *r;
        return y;
    }
}
Failed proof tree
… (200 of 1236 nodes shown)

Source location: tests/borrowck.rs:3398

fn foo(f: Pair) -> () {
    let s: Datum = f.x;
}
Failed proof tree
… (200 of 293 nodes shown)