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 access_permitted( env, assumptions, state, Access::new(AccessKind::Write, place), places_live_on_exit, ) => state

Premise at line 404. Observed failure causes: failed_judgment.

assign
LineCoverageSource
385✗(borrow_check_expr(
env,
assumptions,
state,
expr,
Assignment(place).live_before(env, &state, places_live_on_exit),
) => (value_ty, state))
3942(borrow_check_place_expr(
env,
assumptions,
state,
place,
) => (place, state))
4021(prove_assignable(env, assumptions, state, value_ty, &place.ty) => state)
40411(access_permitted(
env,
assumptions,
state,
Access::new(AccessKind::Write, place),
places_live_on_exit,
) => state)
412N/A(let state = kill_loans(place, state))
413N/A(let state = state.with_initialized(&place.to_place_expression()))
──────── ("assign")
41533(borrow_check_expr(env, assumptions, state, Expr::Assign { place, expr }, places_live_on_exit) => (Ty::unit(), state))

11 tests failed proving this premise:

Source location: tests/borrowck.rs:227

fn foo() -> u32 {
    let x: Pair;
    x.first = 1_u32;
    return 0_u32;
}
Failed proof tree

Source location: tests/borrowck.rs:1901

fn foo() -> i32 {
    exists<'r0, 'r1> {
        let v1: i32 = 0_i32;
        let v2: &'r0 mut i32 = &mut 'r1 v1;
        // This should result in an error
        v1 = 1_i32;
        return *v2;
    }
}
Failed proof tree

Source location: tests/borrowck.rs:1939

fn foo() -> i32 {
    exists<'r0, 'r1> {
        let v1: i32 = 0_i32;
        let v2: &'r0 i32 = &'r1 v1;
        v1 = 1_i32;
        return *v2;
    }
}
Failed proof tree

Source location: tests/borrowck.rs:2735

fn foo() -> u32 {
    exists<'r0, 'r1> {
        let a: u32 = 22_u32;
        let p: &'r0 u32 = &'r1 a;
        'l: loop {
            if true {
                a = 23_u32;
                continue 'l;
            } else {
                break 'l;
            }
        }
        return *p;
    }
}
Failed proof tree

Source location: tests/borrowck.rs:2870

fn foo() -> u32 {
    exists<'r0, 'r1, 'r2> {
        let a: u32 = 22_u32;
        let b: u32 = 22_u32;
        let p: &'r0 u32 = &'r1 a;
        a = 23_u32;
        'l: loop {
            p = &'r2 b;
            break 'l;
        }
        return *p;
    }
}
Failed proof tree

Source location: tests/borrowck.rs:3097

fn foo() -> u32 {
    exists<'r0, 'r1> {
        let p: Point = Point { x: 0_u32, y: 0_u32 };
        let b1: &'r0 mut u32 = &mut 'r1 p.x;
        p.x = 1_u32;
        return *b1;
    }
}
Failed proof tree

Source location: tests/borrowck.rs:3168

fn foo() -> u32 {
    exists<'r0> {
        let v1: u32 = 0_u32;
        let w: Wrapper<'r0> = Wrapper::<'r0> { value: &mut 'r0 v1 };
        v1 = 1_u32;
        return *(w.value);
    }
}
Failed proof tree

Source location: tests/borrowck.rs:3338

fn foo() -> u32 {
    exists<'r0, 'r1, 'r2> {
        let x: u32 = 22_u32;
        let p: &'r1 u32 = &'r0 x;
        let q: &'r2 u32 = p;
        x = 1_u32;
        q;
        return 0_u32;
    }
}
Failed proof tree

Source location: tests/borrowck.rs:3502

fn foo() -> u32 {
    exists<'r0, 'r1> {
        let x: u32 = 22_u32;
        let helper: &'r1 u32 = &'r0 x;
        x = 1_u32;
        helper;
        return 0_u32;
    }
}
Failed proof tree

Source location: tests/borrowck.rs:3751

#[test]
fn issue_63908_remove_last_node_iterative() {
    FormalityTest::new(feature_gate_program(
        NLL_GATE,
        ISSUE_63908_REMOVE_LAST_NODE_ITERATIVE,
    ))
    .skip_execute()
    .err(expect_test::expect![[r#"
        the rule "borrow of disjoint places" at (nll.rs) failed because
          condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
            &loan.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
            &access.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target

        the rule "loan_cannot_outlive" at (nll.rs) failed because
          condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
            outlived_by_loan = {?lt_2, ?lt_3}
            &lifetime.upcast() = ?lt_2

        the rule "write-indirect" at (nll.rs) failed because
          pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `cursor`

        the rule "write-indirect" at (nll.rs) failed because
          condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
            place_accessed = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
            place_loaned_ref = cursor : &?lt_2 mut List"#]]);

    // [polonius]: rustc errors here (known-bug #63908), same as [nll].
    FormalityTest::new(feature_gate_program(
        POLONIUS_ALPHA_GATE,
        ISSUE_63908_REMOVE_LAST_NODE_ITERATIVE,
    ))
    .skip_execute()
    .err(expect_test::expect![[r#"
        the rule "borrow of disjoint places" at (nll.rs) failed because
          condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
            &loan.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
            &access.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target

        the rule "loan_cannot_outlive" at (nll.rs) failed because
          condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
            outlived_by_loan = {?lt_2, ?lt_3}
            &lifetime.upcast() = ?lt_2

        the rule "write-indirect" at (nll.rs) failed because
          pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `cursor`

        the rule "write-indirect" at (nll.rs) failed because
          condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
            place_accessed = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
            place_loaned_ref = cursor : &?lt_2 mut List"#]]);

    // [legacy]: rustc passes.
    FormalityTest::new(feature_gate_program(
        POLONIUS_UNLOCKED_GATE,
        ISSUE_63908_REMOVE_LAST_NODE_ITERATIVE,
    ))
    .skip_execute()
    .ok();
}
Failed proof tree

Source location: tests/borrowck.rs:3776

#[test]
fn issue_63908_remove_last_node_iterative() {
    FormalityTest::new(feature_gate_program(
        NLL_GATE,
        ISSUE_63908_REMOVE_LAST_NODE_ITERATIVE,
    ))
    .skip_execute()
    .err(expect_test::expect![[r#"
        the rule "borrow of disjoint places" at (nll.rs) failed because
          condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
            &loan.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
            &access.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target

        the rule "loan_cannot_outlive" at (nll.rs) failed because
          condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
            outlived_by_loan = {?lt_2, ?lt_3}
            &lifetime.upcast() = ?lt_2

        the rule "write-indirect" at (nll.rs) failed because
          pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `cursor`

        the rule "write-indirect" at (nll.rs) failed because
          condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
            place_accessed = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
            place_loaned_ref = cursor : &?lt_2 mut List"#]]);

    // [polonius]: rustc errors here (known-bug #63908), same as [nll].
    FormalityTest::new(feature_gate_program(
        POLONIUS_ALPHA_GATE,
        ISSUE_63908_REMOVE_LAST_NODE_ITERATIVE,
    ))
    .skip_execute()
    .err(expect_test::expect![[r#"
        the rule "borrow of disjoint places" at (nll.rs) failed because
          condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
            &loan.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
            &access.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target

        the rule "loan_cannot_outlive" at (nll.rs) failed because
          condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
            outlived_by_loan = {?lt_2, ?lt_3}
            &lifetime.upcast() = ?lt_2

        the rule "write-indirect" at (nll.rs) failed because
          pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `cursor`

        the rule "write-indirect" at (nll.rs) failed because
          condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
            place_accessed = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
            place_loaned_ref = cursor : &?lt_2 mut List"#]]);

    // [legacy]: rustc passes.
    FormalityTest::new(feature_gate_program(
        POLONIUS_UNLOCKED_GATE,
        ISSUE_63908_REMOVE_LAST_NODE_ITERATIVE,
    ))
    .skip_execute()
    .ok();
}

Proof trees omitted for the remaining 1 tests.