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: prove_assignable / subtype / premise prove_sub_type(env, assumptions, state, a, b) => state

Premise at line 1150. Observed failure causes: failed_judgment.

subtype
LineCoverageSource
115013(prove_sub_type(env, assumptions, state, a, b) => state)
──────── ("subtype")
1152129(prove_assignable(env, assumptions, state, a, b) => state)

13 tests failed proving this premise:


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

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

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

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

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

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

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

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

Source location: tests/mir_typeck.rs:168 (all coverage from this test)

fn foo (b: bool) -> u32 {
    if b {
        return 1_u32;
    } else {
        return false;
    }
}
Failed proof tree

Source location: tests/mir_typeck.rs:392 (all coverage from this test)

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

Source location: tests/mir_typeck.rs:488 (all coverage from this test)

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

Source location: tests/mir_typeck.rs:601 (all coverage from this test)

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

Source location: tests/mir_typeck.rs:848 (all coverage from this test)

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

Source location: tests/mir_typeck.rs:1218 (all coverage from this test)

fn foo() -> () {
    let x: i32 = 1_i32 + 2_u32;
}
Failed proof tree

Source location: tests/mir_typeck.rs:1270 (all coverage from this test)

fn foo() -> () {
    let x: i32 = 10_i32 - 3_u32;
}

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


Source location: tests/mir_typeck.rs:1323 (all coverage from this test)

fn foo() -> () {
    let x: i32 = 3_i32 * 4_u32;
}

Source location: tests/mir_typeck.rs:1559 (all coverage from this test)

fn foo() -> () {
    let x: u32 = 1_u32;
    x += 2_u8;
}

How to read this page