Negative coverage: check_safety_matches / safety matches / premise if trait_decl.safety == trait_impl.safety
Premise at line 78. Observed failure causes: if_false.
safety matches| Line | Coverage | Source |
|---|---|---|
| 78 | 2 | (if trait_decl.safety == trait_impl.safety) |
| ──────── ("safety matches") | ||
| 80 | 110 | (check_safety_matches(trait_decl, trait_impl) => ()) |
2 tests failed proving this premise:
Source location: tests/decl_safety.rs:63
#[test]
fn unsafe_trait_mismatch() {
FormalityTest::new(crates![crate baguette {
unsafe trait Foo {}
impl Foo for u32 {}
}])
.err(expect_test::expect![[r#"
the rule "safety matches" at (impls.rs) failed because
condition evaluated to false: `trait_decl.safety == trait_impl.safety`"#]])
}Failed proof tree
check_all_crates failedmod.rs:41rule "check all prefixes"mod.rs:53check_crate failedmod.rs:60rule "check crate"mod.rs:73check_crate_item failedmod.rs:163rule "trait impl"mod.rs:178check_trait_impl failedimpls.rs:13rule "check_trait_impl"impls.rs:32check_safety_matches failedimpls.rs:70rule "safety matches"impls.rs:78 (failed: if_false)
Source location: tests/decl_safety.rs:74
#[test]
fn safe_trait_mismatch() {
FormalityTest::new(crates![crate baguette {
trait Foo {}
unsafe impl Foo for u32 {}
}])
.err(expect_test::expect![[r#"
the rule "safety matches" at (impls.rs) failed because
condition evaluated to false: `trait_decl.safety == trait_impl.safety`"#]])
}Failed proof tree
check_all_crates failedmod.rs:41rule "check all prefixes"mod.rs:53check_crate failedmod.rs:60rule "check crate"mod.rs:73check_crate_item failedmod.rs:163rule "trait impl"mod.rs:178check_trait_impl failedimpls.rs:13rule "check_trait_impl"impls.rs:32check_safety_matches failedimpls.rs:70rule "safety matches"impls.rs:78 (failed: if_false)