Negative coverage: check_neg_trait_impl / check_neg_trait_impl / premise fail "negative impls cannot be unsafe"
Premise at line 53. Observed failure causes: explicit_failure.
check_neg_trait_impl| Line | Coverage | Source |
|---|---|---|
| 53 | 2 | (fail "negative impls cannot be unsafe") |
| ──────── ("check_neg_trait_impl") | ||
| 55 | 3 | (check_neg_trait_impl(program, NegTraitImpl { binder: _, safety: Safety::Unsafe }) => ()) |
2 tests failed proving this premise:
Source location: tests/decl_safety.rs:41
#[test]
fn unsafe_trait_negative_impl_mismatch() {
FormalityTest::new(crates![crate baguette {
unsafe trait Foo {}
unsafe impl !Foo for u32 {}
}])
.err(expect_test::expect![[r#"
the rule "check_neg_trait_impl" at (impls.rs) failed because
negative impls cannot be unsafe"#]])
}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 "neg trait impl"mod.rs:197check_neg_trait_impl failedimpls.rs:45rule "check_neg_trait_impl"impls.rs:53 (failed: explicit_failure)
Source location: tests/decl_safety.rs:52
#[test]
fn safe_trait_negative_impl_mismatch() {
FormalityTest::new(crates![crate baguette {
trait Foo {}
unsafe impl !Foo for u32 {}
}])
.err(expect_test::expect![[r#"
the rule "check_neg_trait_impl" at (impls.rs) failed because
negative impls cannot be unsafe"#]])
}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 "neg trait impl"mod.rs:197check_neg_trait_impl failedimpls.rs:45rule "check_neg_trait_impl"impls.rs:53 (failed: explicit_failure)