Negative coverage: borrow_check_expr / place / premise access_permitted(env, assumptions, state, Access::new(access_kind, place), places_live_on_exit) => state

Premise at line 547. Observed failure causes: failed_judgment.

17 tests failed proving this premise:

Source location: src/test_util.rs:464 (all coverage from this test)

#[test]
fn borrowck_err_checks_rustc_err_once() {
    let before = rustc_runs();
    FormalityTest::new(MOVED)
        .rustc_err(expect_test::expect![[r#"
            error[E0382]: use of moved value: `x`
             --> lib.rs
              |
            6 |     let mut x: Datum = Datum { value: 0_u32 };
              |         ----- move occurs because `x` has type `Datum`, which does not implement the `Copy` trait
            7 |     let mut y: Datum = x;
              |                        - value moved here
            8 |     let mut z: Datum = x;
              |                        ^ value used here after move
              |
            note: if `Datum` implemented `Clone`, you could clone the value
             --> lib.rs
              |
            1 | pub struct Datum {
              | ^^^^^^^^^^^^^^^^ consider implementing `Clone` for this type
            ...
            7 |     let mut y: Datum = x;
              |                        - you could clone this value

            For more information about this error, try `rustc --explain E0382`.
            error: could not compile `Foo` (lib) due to 1 previous error
        "#]])
        .borrowck_err(BorrowCheckFailure::All, expect_test::expect![[r#"
            the rule "access_permitted" at (nll.rs) failed because
              condition evaluated to false: `match access.kind
              {
                  AccessKind::Write =>
                  check_place_writable(&state, &access.place.to_place_expression()),
                  AccessKind::Read | AccessKind::Move =>
                  check_place_initialized(&state, &access.place.to_place_expression()),
              }`"#]]);
    assert_eq!(rustc_runs() - before, 1);
}

Source location: src/test_util.rs:479 (all coverage from this test)

#[test]
#[should_panic(expected = "expected `rustc` to succeed but it failed")]
fn borrowck_err_enforces_rustc_ok() {
    FormalityTest::new(MOVED).rustc_ok().borrowck_err(
        BorrowCheckFailure::All,
        expect_test::expect![[r#"
            the rule "access_permitted" at (nll.rs) failed because
              condition evaluated to false: `match access.kind
              {
                  AccessKind::Write =>
                  check_place_writable(&state, &access.place.to_place_expression()),
                  AccessKind::Read | AccessKind::Move =>
                  check_place_initialized(&state, &access.place.to_place_expression()),
              }`"#]],
    );
}

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

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

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

fn foo() -> Datum {
    let x: Datum = Datum { value: 0_u32 };
    let y: Datum = x;
    let z: Datum = x;
    return z;
}

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

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

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

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

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

fn foo() -> Datum {
    let x: Datum = Datum { value: 0_u32 };
    if true {
        let y: Datum = x;
    }
    let z: Datum = x;
    return z;
}

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

fn foo() -> u32 {
    let x: Pair = Pair {
        first: Datum { value: 1_u32 },
        second: Datum { value: 2_u32 },
    };
    let a: Datum = x.first;
    let b: Pair = x;
    return 0_u32;
}

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

fn foo() -> Datum {
    let x: Pair = Pair {
        first: Datum { value: 1_u32 },
        second: Datum { value: 2_u32 },
    };
    let a: Datum = x.first;
    let b: Datum = x.first;
    return b;
}

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

fn foo() -> Datum {
    let x: Pair = Pair {
        first: Datum { value: 1_u32 },
        second: Datum { value: 2_u32 },
    };
    let a: Pair = x;
    let b: Datum = x.first;
    return b;
}

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

fn foo() -> u32 {
    let x: Outer = Outer {
        foo: Inner { bar: 1_u32 },
    };
    let a: Inner = x.foo;
    let b: u32 = x.foo.bar;
    return b;
}

Proof trees omitted for the remaining 7 tests; each one is on its test’s page in Coverage by test.

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

fn foo() -> Datum {
    exists<'r0, 'r1> {
        let x: Datum = Datum { value: 0_u32 };
        let r: &'r0 Datum = &'r1 x;
        let y: Datum = x;
        return *r;
    }
}

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

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

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

fn foo() -> i32 {
    exists<'r0, 'r1> {
        let x: i32 = 0_i32;
        let r: &'r0 i32;
        'a: loop {
            r; // this *may* read from `y` in a previous iteration
            let y: i32 = 0_i32;
            r = &'r1 y;
            continue 'a;
        }
    }
}

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

fn foo() -> u32 {
    exists<'r0, 'r1> {
        let v1: u32 = 22_u32;
        let v2: &'r0 mut u32 = &'r1 mut v1;
        let w: Wrapper = Wrapper { value: v1 };
        return *v2;
    }
}

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

fn foo() -> () {
    let x: u32 = 1_u32;
    exists<'a> {
        let r: &'a mut u32 = &'a mut x;
        x = x + *r;
    }
}

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

fn foo() -> () {
    let x: u32 = 1_u32;
    exists<'a> {
        let r: &'a mut u32 = &'a mut x;
        *r += x;
    }
}

How to read this page