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 / assign-op / premise access_permitted(env, assumptions, state, Access::new(AccessKind::Read, place), places_live_before_write) => state

Premise at line 446. Observed failure causes: failed_judgment.

assign-op
LineCoverageSource
4321(borrow_check_expr(
env,
assumptions,
state,
rhs,
Seq(place, Assignment(place)).live_before(env, &state, places_live_on_exit),
) => (rhs_ty, state))
439N/A(let places_live_before_write = Assignment(place).live_before(env, &state, places_live_on_exit))
441✗(borrow_check_place_expr(env, assumptions, state, place) => (place, state))
442✗(prove_ty_is_rigid(env, assumptions, state, &place.ty) => (RigidTy { name: RigidName::ScalarId(scalar), parameters: _ }, state))
4431(if scalar.is_int())
4441(prove_assignable(env, assumptions, state, rhs_ty, &place.ty) => state)
4462(access_permitted(env, assumptions, state, Access::new(AccessKind::Read, place), places_live_before_write) => state)
4471(access_permitted(env, assumptions, state, Access::new(AccessKind::Write, place), places_live_on_exit) => state)
448N/A(let state = kill_loans(place, state))
──────── ("assign-op")
4507(borrow_check_expr(env, assumptions, state, Expr::AssignOp { place, op: _, rhs }, places_live_on_exit) => (Ty::unit(), state))

2 tests failed proving this premise:

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

fn foo() -> () {
    let x: u32;
    x += 1_u32;
}
Failed proof tree

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

fn foo() -> () {
    let x: u32 = 1_u32;
    exists<'a> {
        let r: &'a mut u32 = &'a mut x;
        x += *r;
        let y: u32 = *r;
    }
}
Failed proof tree

How to read this page