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_statement / return / premise prove_assignable(env, assumptions, state, expr_ty, output_ty) => state

Premise at line 284. Observed failure causes: failed_judgment.

return
LineCoverageSource
2825(borrow_check_expr(env, assumptions, state, expr, LivePlaces::default()) => (expr_ty, state))
283✗(if let Some(output_ty) = &env.output_ty)
2844(prove_assignable(env, assumptions, state, expr_ty, output_ty) => state)
285N/A(let state = state.diverges())
──────── ("return")
28779(borrow_check_statement(env, assumptions, state, Stmt::Return { expr }, _places_live_on_exit) => (env, state))

4 tests failed proving this premise:

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

fn foo<'a, 'b>(v1: &'a u32) -> &'b u32 {
    exists<'r0> {
        let v2: &'r0 u32 = v1;
        return v2;
    }
}
Failed proof tree

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

fn foo<'a, 'b, 'c>(v1: &'a u32) -> &'c u32
where
    'a: 'b,
{
    return v1;
}
Failed proof tree

Source location: tests/mir_typeck.rs:168 (all coverage from this test)

fn foo (b: bool) -> u32 {
    if b {
        return 1_u32;
    } else {
        return false;
    }
}
Failed proof tree

Source location: tests/mir_typeck.rs:601 (all coverage from this test)

fn foo (v1: ()) -> u32 {
    return v1;
}
Failed proof tree

How to read this page