Coverage by test

The same data as the coverage report, organized by test rather than by judgment: each test lists the rules it proves and the premises it is observed to fail on.

`crates/formality-core/src/judgment.rs`

Test	Rules proved	Premises failed
line 19	1	0
line 25	2	0

`crates/formality-core/src/judgment/test_comprehension.rs`

Test	Rules proved	Premises failed
sequence_preserves_order_and_duplicates_while_set_deduplicates (line 44)	1	0
sequence_preserves_order_and_duplicates_while_set_deduplicates (line 45)	1	0
empty_collection_succeeds (line 50)	1	0
empty_collection_succeeds (line 51)	1	0
map_upcasts_both_components_and_replaces_duplicate_keys (line 70)	1	0
map_upcasts_both_components_and_replaces_duplicate_keys (line 73)	1	0
field_projection_implicitly_borrows_and_clones (line 105)	1	0
later_use_infers_collection_and_element_types (line 123)	1	0
premises_preserve_each_successful_subproof (line 157)	2	0
failed_premises_fail_instead_of_filtering (line 181)	0	2
failed_premises_fail_instead_of_filtering (line 184)	0	1
failed_premises_fail_instead_of_filtering (line 187)	1	0
terminal_judgment_implicitly_upcasts_its_result_and_propagates_failure (line 206)	2	0
terminal_judgment_implicitly_upcasts_its_result_and_propagates_failure (line 207)	0	2
terminal_judgment_can_use_preceding_bindings (line 229)	2	0
terminal_judgment_can_use_preceding_bindings (line 230)	0	2
destructured_judgment_result_can_feed_an_explicit_final_expression (line 264)	3	0
collection_and_final_value_accept_compound_expressions (line 285)	1	0
question_mark_in_yield_propagates_failure (line 309)	1	0
question_mark_in_yield_propagates_failure (line 310)	0	1
parentheses_or_a_block_can_wrap_a_tail_that_starts_with_parentheses (line 334)	1	0
tuple_tail_after_premises_needs_only_its_own_parentheses (line 356)	2	0
conditional_tail_is_a_rust_expression (line 379)	1	0
unit_and_wrapped_negation_are_valid_final_expressions (line 403)	1	0
premise_commit_marker_is_preserved_before_a_tail (line 426)	2	0
premise_commit_marker_is_preserved_before_a_tail (line 427)	0	2
nested_comprehensions_have_independent_accumulators (line 450)	1	0
ordinary_array_expressions_still_work (line 544)	1	0

`crates/formality-core/src/judgment/test_explicit_fail.rs`

Test	Rules proved	Premises failed
local_can_be_moved (line 39)	1	0
deref_explicit_failure_message (line 44)	0	1

`crates/formality-core/src/judgment/test_fallible.rs`

Test	Rules proved	Premises failed
is_equal_22 (line 58)	1	0
is_equal_44 (line 63)	2	0
is_not_equal (line 68)	0	1

`crates/formality-core/src/judgment/test_filtered.rs`

Test	Rules proved	Premises failed
judgment (line 51)	0	1
judgment (line 55)	2	0

`crates/formality-core/src/judgment/test_for_all.rs`

Test	Rules proved	Premises failed
test_for_all_success (line 37)	1	0
test_for_all_failure (line 43)	0	1
test_for_all_empty (line 51)	1	0
test_for_all_with_accumulator (line 74)	1	0
test_for_all_with_accumulator_empty (line 80)	1	0
test_ordinary_premises_preserve_alternatives (line 135)	2	0
test_ordinary_premises_preserve_alternatives (line 136)	3	0
test_for_all_with_accumulator_preserves_alternatives (line 141)	3	0
test_for_all_with_accumulator_returns_all_alternatives (line 146)	3	0
test_for_all_merges_equivalent_states (line 182)	2	0
test_for_all_continuation_filters_alternatives_and_preserves_proof (line 204)	2	0

`crates/formality-core/src/judgment/test_reachable.rs`

Test	Rules proved	Premises failed
judgment (line 51)	2	0

`crates/formality-core/src/judgment/test_scope.rs`

Test	Rules proved	Premises failed
test_scope_each_proof_leaves (line 64)	1	0
test_scope_some_proofs_cannot_leave (line 71)	1	0
test_scope_no_proof_can_leave (line 77)	0	1
test_scope_with_two_variables (line 112)	1	0
test_scope_entered (line 141)	1	0
test_scope_not_entered (line 147)	0	1
test_scope_leave_proves_several (line 191)	1	0
test_scope_with_no_variables (line 222)	1	0
test_scope_with_no_variables_unproven (line 229)	0	1
test_scope_nested_with_variables (line 255)	1	0

`crates/formality-rust/src/prove/test/adt_wf.rs`

Test	Rules proved	Premises failed
well_formed_adt (line 30)	8	0
not_well_formed_adt (line 44)	0	11

`crates/formality-rust/src/prove/test/eq_assumptions.rs`

Test	Rules proved	Premises failed
test_a (line 15)	12	0
test_b (line 24)	12	0
test_normalize_assoc_ty (line 33)	7	0
test_normalize_assoc_ty_existential0 (line 41)	0	19
test_normalize_assoc_ty_existential1 (line 126)	11	0

`crates/formality-rust/src/prove/test/eq_partial_eq.rs`

Test	Rules proved	Premises failed
eq_implies_partial_eq (line 25)	11	0
not_partial_eq_implies_eq (line 33)	0	5
universals_not_eq (line 44)	0	12

`crates/formality-rust/src/prove/test/exists_constraints.rs`

Test	Rules proved	Premises failed
exists_u_for_t (line 24)	7	0

`crates/formality-rust/src/prove/test/expanding.rs`

Test	Rules proved	Premises failed
expanding (line 23)	4	0

`crates/formality-rust/src/prove/test/is_local.rs`

Test	Rules proved	Premises failed
test_forall_not_local (line 11)	0	6
test_exists_not_local (line 26)	6	0

`crates/formality-rust/src/prove/test/magic_copy.rs`

Test	Rules proved	Premises failed
all_t_not_magic (line 25)	0	12
all_t_not_copy (line 40)	0	12

`crates/formality-rust/src/prove/test/occurs_check.rs`

Test	Rules proved	Premises failed
direct_cycle (line 24)	0	6
eq_variable_to_rigid (line 36)	6	0
eq_rigid_to_variable (line 42)	7	0
indirect_cycle_1 (line 48)	0	8
indirect_cycle_2 (line 60)	0	8

`crates/formality-rust/src/prove/test/simple_impl.rs`

Test	Rules proved	Premises failed
vec_u32_debug (line 24)	9	0
vec_vec_u32_debug (line 30)	9	0

`crates/formality-rust/src/prove/test/universes.rs`

Test	Rules proved	Premises failed
exists_u_for_t (line 14)	0	8
for_t_exists_u (line 37)	9	0

`src/test_util.rs`

Test	Rules proved	Premises failed
borrowck_ok_checks_rustc_ok_once (line 423)	58	0
borrowck_ok_enforces_rustc_err (line 434)	58	0
borrowck_err_checks_rustc_err_once (line 464)	0	12
borrowck_err_enforces_rustc_ok (line 479)	0	12
rustc_expectation_is_independent_of_borrowck_modes (line 516)	85	27

`tests/associated_type_normalization.rs`

Test	Rules proved	Premises failed
test_mirror_normalizes_u32_to_u32 (line 19)	9	0

`tests/basic_tests.rs`

Test	Rules proved	Premises failed
hello_world_fail (line 34)	0	9
hello_world (line 58)	41	0
basic_where_clauses_pass (line 74)	26	0
basic_where_clauses_fail (line 85)	0	11
basic_where_clauses_without_lifetime_binders_feature_flag_fail (line 103)	0	2
foo (line 121)	32	0
foo (line 133)	0	2
non_lifetime_binder_in_trait_impl_where_clause_pass (line 149)	29	0
non_lifetime_binder_in_trait_impl_where_clause_fail (line 161)	0	2
non_lifetime_binder_in_neg_trait_impl_where_clause_pass (line 179)	33	0
non_lifetime_binder_in_neg_trait_impl_where_clause_fail (line 191)	0	2
non_lifetime_binder_in_enum_where_clause_pass (line 209)	28	0
non_lifetime_binder_in_enum_where_clause_fail (line 221)	0	2
non_lifetime_binder_in_struct_where_clause_pass (line 239)	28	0
non_lifetime_binder_in_struct_where_clause_fail (line 251)	0	2
lifetime_binder_in_where_clause_without_feature_pass (line 266)	25	0
basic_adt_variant_dup (line 277)	0	4
basic_adt_field_dup (line 290)	0	4
line 303	0	4
trait_items_with_duplicate_associated_type_names (line 316)	0	4
crate_with_duplicate_item_names (line 328)	0	2
crate_with_duplicate_item_names (line 337)	0	2
a (line 346)	0	2
a (line 356)	14	0
basic_impl_dup (line 367)	0	2
basic_neg_impl_dup (line 380)	0	2
line 397	0	4
line 411	0	4
line 425	0	4
line 442	0	4
line 457	26	0
nonexistant_trait (line 466)	0	4

`tests/borrowck.rs`

Test	Rules proved	Premises failed
main (line 23)	47	0
example (line 35)	45	0
main (line 45)	47	0
main (line 55)	47	0
main (line 65)	47	0
main (line 75)	47	0
main (line 84)	47	0
example (line 96)	45	0
foo (line 124)	0	11
foo (line 172)	0	12
foo (line 214)	64	0
foo (line 240)	0	11
foo (line 290)	62	0
foo (line 316)	61	0
foo (line 342)	0	11
foo (line 393)	0	12
reborrow (line 420)	73	0
foo (line 446)	0	11
foo (line 495)	65	0
foo (line 532)	0	12
foo (line 580)	0	12
foo (line 628)	0	12
foo (line 672)	0	12
foo (line 721)	0	26
foo (line 1476)	0	26
foo (line 2232)	0	25
foo (line 2301)	0	11
foo (line 2347)	0	25
foo (line 2385)	0	25
foo (line 2419)	0	25
min_problem_case_3 (line 2470)	85	27
foo (line 2531)	0	25
foo (line 2575)	86	0
foo (line 2603)	0	25
foo (line 2645)	0	25
min_problem_case_3 (line 2690)	85	0
foo (line 2704)	0	19
foo (line 2734)	0	19
foo (line 2768)	67	0
foo (line 2785)	58	0
foo (line 2799)	0	16
min_problem_case_4 (line 2827)	82	0
foo (line 2963)	86	0
foo (line 2983)	0	26
foo (line 3030)	0	17
foo (line 3100)	0	27
foo (line 3156)	80	0
foo (line 3184)	53	0
foo (line 3227)	0	29
foo (line 3288)	85	27
foo (line 3352)	0	25
foo (line 3393)	70	0
bar (line 3415)	76	0
foo (line 3445)	64	0
foo (line 3470)	0	18
foo (line 3493)	62	0
bar (line 3514)	80	0
bar (line 3536)	0	27
foo (line 3568)	77	0
foo (line 3584)	0	25
foo (line 3618)	0	26
foo (line 3658)	0	25
reborrow (line 3690)	74	0
reborrow (line 3715)	83	26
reborrow (line 3764)	72	0
reborrow (line 3784)	74	0
foo (line 3813)	0	24
foo (line 3869)	72	0
foo (line 3891)	0	22
foo (line 4007)	0	24
foo (line 4035)	0	16
foo (line 4048)	70	0
remove_last_node_recursive (line 4167)	93	0
remove_last_node_iterative (line 4214)	93	24
no_control_flow (line 4276)	91	0
conditional (line 4326)	94	30
conditional_with_indirection (line 4415)	102	0
to_refs (line 4467)	92	0
to_refs2 (line 4502)	93	0
to_refs3 (line 4549)	93	0
next (line 4592)	98	32
next (line 4715)	103	32
use_it (line 4831)	72	21
use_both (line 4862)	0	21
use_it_but_its_the_same_region (line 4896)	77	0
f (line 4970)	79	0
foo (line 4985)	61	0
foo (line 5004)	70	0
foo (line 5022)	76	0
foo (line 5052)	0	25
foo (line 5096)	0	11
bump (line 5120)	61	0
foo (line 5149)	0	26
foo (line 5201)	0	24
foo (line 5253)	0	25

`tests/codegen.rs`

Test	Rules proved	Premises failed
main (line 12)	46	0
main (line 22)	46	0
main (line 33)	46	0
main (line 43)	46	0
example (line 55)	44	0
main (line 63)	46	0
main (line 73)	46	0
main (line 83)	46	0
example (line 95)	44	0
main (line 106)	46	0
main (line 119)	48	0
main (line 131)	57	0
main (line 144)	59	0
main (line 159)	62	0
main (line 174)	62	0
main (line 190)	59	0
main (line 205)	61	0
main (line 222)	59	0
main (line 236)	64	0
main (line 251)	69	0
main (line 265)	57	0
main (line 282)	62	0
main (line 295)	62	0
main (line 312)	62	0
main (line 332)	64	0
main (line 345)	63	0
main (line 358)	64	0
main (line 374)	75	0
main (line 391)	76	0
main (line 410)	64	0
main (line 428)	50	0
main (line 448)	55	0
main (line 469)	65	0
main (line 485)	72	0
main (line 501)	75	0
main (line 516)	69	0
main (line 532)	63	0
main (line 550)	64	0
main (line 566)	48	0
main (line 586)	74	0
main (line 598)	59	0
main (line 611)	61	0
main (line 628)	67	0
main (line 640)	56	0
main (line 653)	62	0
main (line 677)	57	0
main (line 693)	68	0
main (line 705)	51	0
main (line 721)	67	0
main (line 733)	51	0
main (line 745)	51	0
main (line 757)	51	0
main (line 769)	56	0
main (line 781)	51	0
main (line 798)	63	0
main (line 810)	52	0
main (line 822)	52	0
main (line 836)	62	0
main (line 891)	52	0
main (line 905)	52	0
main (line 927)	68	0
main (line 964)	82	0
main (line 976)	52	0
main (line 988)	52	0
main (line 1000)	57	0
main (line 1013)	53	0
main (line 1026)	53	0
main (line 1086)	61	0
main (line 1102)	66	0
main (line 1116)	61	0
main (line 1132)	69	0

`tests/coherence_orphan.rs`

Test	Rules proved	Premises failed
neg_CoreTrait_for_CoreStruct_in_Foo (line 13)	0	11
mirror_CoreStruct (line 48)	0	12
mirror_FooStruct (line 85)	35	0
covered_VecT (line 99)	26	0
main (line 114)	40	0
main (line 129)	40	0
uncovered_mut_ref_T (line 141)	0	16
uncovered_nested_ref_T (line 172)	0	16
raw_pointer_is_not_fundamental (line 213)	0	10
uncovered_T (line 235)	0	11
uncovered_ref_T (line 254)	0	14
main (line 286)	32	0
main (line 300)	38	0
ref_foreign_wrapper_of_local_is_not_local (line 329)	0	12
ref_CoreStruct_is_not_local (line 375)	0	12
alias_to_unit (line 412)	0	11
CoreTrait_for_CoreStruct_in_Foo (line 434)	0	11
CoreTraitLocal_for_AliasToKnown_in_Foo (line 472)	36	0

`tests/coherence_overlap.rs`

Test	Rules proved	Premises failed
u32_not_u32_impls (line 218)	0	4
neg_CoreTrait_for_CoreStruct_implies_no_overlap (line 237)	37	0
foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait (line 251)	0	10
T_where_Foo_not_u32_impls (line 277)	0	4
u32_T_where_T_Is_impls (line 292)	0	10
u32_T_where_T_Not_impls (line 322)	26	0
u32_u32_impls (line 332)	0	2
u32_i32_impls (line 345)	19	0
u32_T_impls (line 355)	0	7
T_where_Bar_and_ref_T (line 394)	0	10
T_where_Bar_and_mut_ref_T (line 437)	0	10
T_where_Bar_and_nested_ref_T (line 480)	0	10
T_and_T_bar (line 511)	0	10
T_and_Local_Bar_T (line 544)	0	10
is_local_unknowable_trait_ref (line 587)	35	0
is_local_with_unconstrained_self_ty_blanket_impl (line 613)	0	10

`tests/const_generics_rv_tsv_parse.rs`

Test	Rules proved	Premises failed
parse_minirust_22 (line 12)	41	0

`tests/consts.rs`

Test	Rules proved	Premises failed
nonsense_rigid_const_bound (line 10)	0	4
ok (line 27)	41	0
mismatch (line 36)	0	12
holds (line 53)	41	0
rigid_const_bound (line 61)	0	4
generic_mismatch (line 76)	0	15
generic_match (line 100)	41	0
multiple_type_of_const (line 109)	39	0
nested_const_bound_rejects_fixed_value (line 117)	0	4
nested_const_bound_accepts_outer_parameter (line 131)	40	0
nested_const_bound_accepts_inner_parameter (line 141)	41	0
line 149	0	5
line 166	54	0

`tests/decl_safety.rs`

Test	Rules proved	Premises failed
unsafe_trait (line 13)	38	0
safe_trait (line 24)	38	0
unsafe_trait_negative_impl (line 36)	43	0
unsafe_trait_negative_impl_mismatch (line 59)	0	4
safe_trait_negative_impl_mismatch (line 84)	0	4
unsafe_trait_mismatch (line 111)	0	5
safe_trait_mismatch (line 138)	0	5

`tests/drop.rs`

Test	Rules proved	Premises failed
line 23	53	0
line 43	54	0
line 61	51	0
line 83	0	13
line 108	52	0
line 128	53	0
drop_impl_missing_drop_fn (line 159)	0	4
drop (line 192)	0	10
drop (line 228)	0	10
line 250	0	9
line 274	0	13
line 313	0	9
line 338	0	4
line 353	0	4

`tests/field_projections.rs`

Test	Rules proved	Premises failed
test (line 17)	64	0

`tests/functions.rs`

Test	Rules proved	Premises failed
multi_arg_ret (line 25)	41	0
one_lt_arg (line 39)	41	0
line 55	41	0
main (line 70)	51	0

`tests/judgment-error-reporting/cyclic_judgment.rs`

Test	Rules proved	Premises failed
test (line 73)	0	3
test1 (line 133)	0	4

`tests/mir_typeck.rs`

Test	Rules proved	Premises failed
foo (line 14)	54	0
foo (line 37)	53	0
foo (line 93)	54	0
foo (line 110)	60	0
foo (line 123)	49	0
foo (line 140)	57	0
foo (line 168)	0	15
bar (line 193)	60	0
foo (line 214)	54	0
foo (line 259)	66	0
foo (line 276)	50	0
foo (line 321)	0	14
bar (line 345)	0	15
bar (line 392)	0	17
bar (line 416)	0	15
bar (line 439)	60	0
bar (line 488)	0	17
bar (line 532)	0	11
bar (line 568)	0	13
foo (line 601)	0	14
foo (line 791)	0	11
foo (line 820)	0	11
foo (line 848)	0	17
foo (line 876)	0	11
main (line 902)	0	11
foo (line 925)	57	0
foo (line 949)	61	0
foo (line 967)	71	0
foo (line 987)	65	0
foo (line 1014)	53	0
foo (line 1046)	0	11
foo (line 1073)	53	0
foo (line 1109)	0	10
foo (line 1142)	70	0
foo (line 1168)	51	0
foo (line 1218)	0	17
foo (line 1270)	0	17
foo (line 1323)	0	18
foo (line 1349)	0	12
main (line 1394)	0	13
main (line 1438)	0	14
main (line 1453)	48	0
main (line 1466)	52	0
main (line 1478)	49	0
main (line 1489)	49	0
main (line 1514)	0	16
foo (line 1559)	0	15
foo (line 1586)	0	10

`tests/projection.rs`

Test	Rules proved	Premises failed
normalize_basic (line 25)	11	0
normalize_basic (line 31)	11	0
normalize_basic (line 36)	5	0
normalize_basic (line 44)	7	0
normalize_basic (line 50)	4	0
normalize_basic (line 55)	11	0
normalize_into_iterator (line 89)	11	0
projection_equality (line 112)	10	0
projection_equality (line 115)	12	0

`tests/references.rs`

Test	Rules proved	Premises failed
line 13	0	12
line 36	29	0

`tests/return_validation.rs`

Test	Rules proved	Premises failed
foo (line 33)	44	0
foo (line 51)	57	0
foo (line 84)	47	0
foo (line 118)	53	0
foo (line 132)	49	0

`tests/sized_trait.rs`

Test	Rules proved	Premises failed
main (line 14)	45	0
sized_bound_not_met_by_unimplemented_type (line 27)	0	14
line 142	54	0
line 153	45	0
line 164	45	0
line 175	47	0
generic_parameter_requires_explicit_sized_bound (line 187)	0	14

`tests/traits.rs`

Test	Rules proved	Premises failed
main (line 11)	51	0
main (line 22)	51	0
line 36	14	0
trait_with_valid_associated_type (line 50)	8	0
associated_type_static_outlives_bound (line 78)	38	0
associated_type_outer_lifetime_outlives_bound (line 88)	38	0
associated_type_trait_and_outlives_bounds (line 99)	38	0

`tests/well_formed_struct.rs`

Test	Rules proved	Premises failed
main (line 17)	68	0

`tests/well_formed_trait_ref.rs`

Test	Rules proved	Premises failed
dependent_where_clause (line 19)	44	0
missing_dependent_where_clause (line 37)	0	10
lifetime_param (line 56)	42	0
static_lifetime_param (line 71)	43	0
const_param (line 86)	46	0

How to read this page

Keyboard shortcuts

A MIR Formality