Negative coverage: check_adt / check adt / premise check_adt_variant_names_unique(adt) => ()
Premise at line 18. Observed failure causes: inapplicable.
check adt| Line | Coverage | Source |
|---|---|---|
| 18 | 2 | (check_adt_variant_names_unique(adt) => ()) |
| 19 | ✗ | (scope(enter_universally(Env::default(), &adt.binder) => (env, AdtBoundData { where_clauses, variants })) with() (prove_where_clauses_well_formed(program, env, where_clauses, where_clauses) => ()) (for_all(variant in variants) (let Variant { fields, .. } = variant) (for_all(field in fields) (let Field { ty, .. } = field) (prove_goal(program, env, where_clauses, AtomicPredicate::well_formed(ty)) => ())))) |
| ──────── ("check adt") | ||
| 27 | 59 | (check_adt(program, adt) => ()) |
2 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)