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 borrow_check_expr(env, assumptions, state, expr, LivePlaces::default()) => (expr_ty, state)

Premise at line 280. Observed failure causes: failed_judgment.

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

5 tests failed proving this premise:

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

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

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

fn foo() -> u32 {
    let x: u32;
    if true {
        x = 1_u32;
    } else {
    }
    return x;
}
Failed proof tree

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

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

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

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

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

fn use_it<'a, 'b>() -> u32 {
    exists<'r0> {
        let v: Invariant<'r0> = create_invariant::<'r0>();
        if true {
            return sink::<'a, 'r0>(v);
        } else {
            return sink::<'b, 'r0>(v);
        }
    }
}