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

Premise at line 362. Observed failure causes: failed_judgment.

assign
LineCoverageSource
353✗(borrow_check_expr(
env,
assumptions,
state,
expr,
Assignment(place).live_before(env, &state, places_live_on_exit),
) => (value_ty, state))
3622(borrow_check_place_expr(
env,
assumptions,
state,
place,
) => (place, state))
3701(prove_assignable(env, assumptions, state, value_ty, &place.ty) => state)
3728(access_permitted(
env,
assumptions,
state,
Access::new(AccessKind::Write, place),
places_live_on_exit,
) => state)
380N/A(let state = kill_loans(place, state))
381N/A(let state = state.with_initialized(&place.to_place_expression()))
──────── ("assign")
38313(borrow_check_expr(env, assumptions, state, Expr::Assign { place, expr }, places_live_on_exit) => (Ty::unit(), state))

2 tests failed proving this premise:

Source location: tests/mir_typeck.rs:595

fn foo (v1: u32) -> u32 {
    let v2: Dummy = Dummy { value: 1 _ u32 };
    v2.nonexistent = 2 _ u32;
    return v1;
}
Failed proof tree

Source location: tests/mir_typeck.rs:613

fn foo (v1: u32) -> u32 {
    let v2: Dummy = Dummy { value: 1 _ u32 };
    v1.value = 2 _ u32;
    return v1;
}
Failed proof tree