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 / ref / premise verify_universal_outlives(env, assumptions, &state.current.outlives) => ()

Premise at line 495. Observed failure causes: failed_judgment.

ref
LineCoverageSource
466✗(borrow_check_place_expr(
env,
assumptions,
state,
place,
) => (place, state))
474N/A(let access_kind = match kind {
RefKind::Shared => AccessKind::Read,
RefKind::Mut => AccessKind::Write,
})
4788(access_permitted(
env,
assumptions,
state,
Access::new(access_kind, place),
places_live_on_exit,
) => state)
487N/A(let state = state.with_loan(Loan::new(lt, place, kind)))
488N/A(let state = state.with_outlives(&reborrow_constraints(place, lt)))
4951(verify_universal_outlives(env, assumptions, &state.current.outlives) => ())
496N/A(let ty = place.ty.ref_ty_of_kind(kind, lt))
──────── ("ref")
49845(borrow_check_expr(env, assumptions, state, Expr::Ref { kind, lt, place }, places_live_on_exit) => (ty, state))

1 test failed proving this premise:

Source location: tests/borrowck.rs:3527

fn foo<'a, 'b>(p: &'a mut u32) -> u32 {
    let q: &'b mut u32 = &mut 'b *p;
    q;
    return 0_u32;
}
Failed proof tree