Negative coverage: prove_predicate / subtype / premise prove_sub(decls, env, assumptions, a, b) => c

Premise at line 121. Observed failure causes: failed_judgment.

11 tests failed proving this premise:

Source location: tests/drop.rs:192 (all coverage from this test)

fn drop<'a>(self: &'a MyStruct) -> () {}
}
}])
rr(expect_test::expect![[r#"
r[E0053]: method `drop` has an incompatible type for trait
 lib.rs
|
    fn drop<'a10>(mut self: &'a10 MyStruct) -> () {}
                            ^^^^^^^^^^^^^^ types differ in mutability
|
note: expected signature `fn(&mut MyStruct)`
         found signature `fn(&MyStruct)`
: change the self-receiver type to match the trait
|
    fn drop<'a10>(mut self: &'a10 MyStruct) -> () {}
    fn drop<'a10>(mut &mut self) -> () {}
|

more information about this error, try `rustc --explain E0053`.
r: could not compile `Foo` (lib) due to 1 previous error
"#]])
ect_test::expect![[r#"
es/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: &!lt_0 mut MyStruct, assumptions: {}, env: Env { variables: [!lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }

es/formality-rust/src/prove/prove_normalize.rs:22:1: no applicable rules for prove_normalize { p: &!lt_0 MyStruct, assumptions: {}, env: Env { variables: [!lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
}

ust return unit, even when its body matches another return type.
#[test]
_non_unit_return() {
yTest::new(crates![crate Foo {
ct MyStruct {}

 Drop for MyStruct {
fn drop<'a>(self: &'a mut MyStruct) -> u32 {
    return 0_u32;
}

Source location: tests/drop.rs:228 (all coverage from this test)

fn drop<'a>(self: &'a mut MyStruct) -> u32 {
    return 0_u32;
}

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

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

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

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

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

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

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

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

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

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

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

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

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

How to read this page