Negative coverage: check_crate_item / adt / premise check_adt(program, &s.to_adt()) => ()
Premise at line 201. Observed failure causes: failed_judgment.
adt| Line | Coverage | Source |
|---|---|---|
| 201 | 3 | (check_adt(program, &s.to_adt()) => ()) |
| ──────── ("adt") | ||
| 203 | 59 | (check_crate_item(program, CrateItem::AdtItem(s), crate_id) => ()) |
3 tests failed proving this premise:
Source location: tests/basic_tests.rs:277 (all coverage from this test)
#[test]
fn basic_adt_variant_dup() {
FormalityTest::new(crates![crate Foo {
enum Bar {
Baz{},
Baz{},
}
}])
.err(expect_test::expect![[r#"
the rule "check adt" at (adts.rs) failed because
variant "Baz" defined multiple times"#]])
}Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "adt"mod.rs:201check_adt failedadts.rs:11args
rule "check adt"adts.rs:18 (failed: inapplicable)
Source location: tests/basic_tests.rs:290 (all coverage from this test)
#[test]
fn basic_adt_field_dup() {
FormalityTest::new(crates![crate Foo {
struct Bar {
baz: (),
baz: (),
}
}])
.err(expect_test::expect![[r#"
the rule "check adt" at (adts.rs) failed because
field "baz" of variant "struct" defined multiple times"#]])
}Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "adt"mod.rs:201check_adt failedadts.rs:11args
rule "check adt"adts.rs:18 (failed: inapplicable)
Source location: tests/well_formed_trait_ref.rs:37 (all coverage from this test)
#[test]
fn missing_dependent_where_clause() {
FormalityTest::new(crates![crate foo {
trait Trait1 {}
trait Trait2 {}
struct S1<T> where T: Trait1 {
dummy: T,
}
struct S2<T> where S1<T> : Trait2 {
dummy: T,
}
}])
.err(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: @ WellFormedTraitRef(Trait2(S1<!ty_0>)), via: Trait2(S1<!ty_0>), assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: Trait1(!ty_0), via: Trait2(S1<!ty_0>), assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
the rule "trait implied bound" at (prove_predicate.rs) failed because
expression evaluated to an empty collection: `decls.trait_invariants()`"#]])
}Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "adt"mod.rs:201check_adt failedadts.rs:11args
rule "check adt"adts.rs:20prove failedfunction.rs:250args
rulefunction.rs:250prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "trait well formed"prove_predicate.rs:127prove_wf failedprove_wf.rs:11args
rule "ADT"prove_wf.rs:64prove_after failedprove_after.rs:8args
rule "prove_after"prove_after.rs:19prove failedprove_after.rs:19args
ruleprove_after.rs:19prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "trait implied bound"prove_predicate.rs:106 (failed: empty_collection)