Negative coverage: borrow_check_expr_has_ty / block / premise borrow_check_expr(env, assumptions, state, expr, places_live_on_exit) => (ty_expr, state)

Premise at line 332. Observed failure causes: failed_judgment.

19 tests failed proving this premise:

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

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

Source location: tests/borrowck.rs:1112

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

Source location: tests/borrowck.rs:1772

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

fn foo<'a, 'b>(a: &'a u32) -> &'b u32 {
    let r: &'b u32 = identity::<&'b u32>(a);
    return r;
}

Source location: tests/borrowck.rs:2944

fn bar() -> u32 {
    exists<'r0, 'r1, 'r2> {
        let v: u32 = 0 _ u32;
        let p: &'r0 u32 = &'r1 v;
        let _: u32 = foo::<'r2>(&mut 'r2 v);
        return *p;
    }
}

Source location: tests/borrowck.rs:3026

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

Proof trees omitted for the remaining 9 tests.

Source location: tests/mir_typeck.rs:280

fn bar() -> u32 {
    let v1: u32 = foo(0 _ u32);
    return v1;
}

Source location: tests/mir_typeck.rs:300

fn bar(v1: ()) -> () {
    let v0: () = foo(v1);
    return v0;
}

Source location: tests/mir_typeck.rs:323

fn bar(v1: u32) -> u32 {
    let v0: u32 = identity(v1);
    return v0;
}

Source location: tests/mir_typeck.rs:360

fn bar(v1: u32) -> u32 {
    let v0: u32 = identity::<bool>(v1);
    return v0;
}

Source location: tests/mir_typeck.rs:383

fn bar(v1: u32) -> u32 {
    let v0: u32 = identity::<u32>(v1, v1);
    return v0;
}

Source location: tests/mir_typeck.rs:401

fn bar(v1: u32) -> u32 {
    let v0: u32 = identity::<u32, u32>(v1);
    return v0;
}

Source location: tests/mir_typeck.rs:630

fn foo (v1: u32) -> u32 {
    let v2: Dummy = Dummy { value: false };
    return v1;
}

Source location: tests/mir_typeck.rs:648

fn foo (v1: u32) -> u32 {
    let v2: u32 = Nonexistent { value: false };
    return v1;
}