Negative coverage: check_fn / check fn / premise check_fn_body(program, env, assumptions, body, input_args, output_ty) => ()

Premise at line 55. Observed failure causes: failed_judgment.

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

Proof trees omitted for the remaining 36 tests.

Source location: tests/borrowck.rs:1838

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

Source location: tests/borrowck.rs:1881

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

Source location: tests/borrowck.rs:1919

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

Source location: tests/borrowck.rs:1997

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

Source location: tests/borrowck.rs:2069

fn foo() -> i32 {
    exists<'r0, 'r1> {
        let v2: &mut 'r0 i32;
        {
            let v1: i32 = 0 _ i32;
            v2 = &mut 'r1 v1;
        }
        return *v2;
    }
}

Source location: tests/borrowck.rs:2111

fn foo() -> i32 {
    exists<'r0, 'r1> {
        let v2: &'r0 i32;
        'a: {
            let v1: i32 = 0 _ i32;
            v2 = &'r1 v1;
            break 'a;
        }
        return *v2;
    }
}

Source location: tests/borrowck.rs:2170

fn foo<'a, 'b>(v1: &'a u32) -> &'b u32 {
    exists<'r0> {
        let v2: &'r0 u32 = v1;
        return v2;
    }
}

Source location: tests/borrowck.rs:2192

fn foo<'a, 'b>(v1: &'a u32, v2: &'b u32) -> () {
    let output: &'b u32 = v2;
    loop {
        output = v1;
    }
}

Source location: tests/borrowck.rs:2249

fn foo<'a, 'b, 'c>(v1: &'a u32) -> &'c u32
where
    'a: 'b,
{
    return v1;
}

Source location: tests/borrowck.rs:2430

fn foo() -> i32 {
    exists<'r0, 'r1> {
        let r: &'r0 i32;
        'a: loop {
            let y: i32 = 0 _ i32;
            r = &'r1 y;
            continue 'a;
        }
        r; // only an error because of false edges, assumption that all loops terminate
    }
}

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

Source location: tests/borrowck.rs:2544

fn foo() -> i32 {
    exists<'r0, 'r1> {
        let r: &'r0 i32;
        'a: loop {
            let x: i32 = 0 _ i32;
            r = &'r1 x;
            break 'a;
        }
        return *r;
    }
}

Source location: tests/borrowck.rs:2671

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

Source location: tests/borrowck.rs:2765

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

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

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

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

Source location: tests/borrowck.rs:3063

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

Source location: tests/borrowck.rs:3185

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

Source location: tests/mir_typeck.rs:147

fn foo (b: bool) -> u32 {
    if b {
        return 1 _ u32;
    } else {
        return false;
    }
}

Source location: tests/mir_typeck.rs:266

fn foo() -> () {
    let s2: S2<S1>;
}

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

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

Source location: tests/mir_typeck.rs:595

fn foo (v1: u32) -> u32 {
    let v2: Dummy = Dummy { value: 1 _ u32 };
    v2.nonexistent = 2 _ u32;
    return v1;
}

Source location: tests/mir_typeck.rs:613

fn foo (v1: u32) -> u32 {
    let v2: Dummy = Dummy { value: 1 _ u32 };
    v1.value = 2 _ u32;
    return v1;
}

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

Source location: tests/mir_typeck.rs:776

fn foo() -> u32 {
    loop {
        break 'nonexistent;
    }
    return 0 _ u32;
}

Source location: tests/mir_typeck.rs:825

fn foo() -> u32 {
    'a: {
        continue 'a;
    }
    return 0 _ u32;
}