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_sub / normalize-l / premise prove_normalize(decls, env, assumptions, x) => Constrained(y, c)

Premise at line 27. Observed failure causes: failed_judgment.

normalize-l
LineCoverageSource
275(prove_normalize(decls, env, assumptions, x) => Constrained(y, c))
28(prove_after(decls, c, assumptions, Predicate::sub(y, z)) => c)
──────── ("normalize-l")
3025(prove_sub(decls, env, assumptions, x, z) => c)

5 tests failed proving this premise:


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