Negative coverage: access_permitted / access_permitted / premise if 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()), }

Premise at line 702. Observed failure causes: if_false.

10 tests failed proving this premise:

Source location: tests/borrowck.rs:29

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

Source location: tests/borrowck.rs:74

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:139

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

Source location: tests/borrowck.rs:212

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

Source location: tests/borrowck.rs:286

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:327

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:368

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:407

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;
}

Source location: tests/borrowck.rs:1838

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

Source location: tests/borrowck.rs:2477

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;
        }
    }
}