Test `tests/functions.rs:25`

Source location: tests/functions.rs:25

Rules proved (37)

Judgment	Rule	All tests of this rule
check_all_crates	check all prefixes	131 tests
check_associated_ty	check associated ty	116 tests
check_associated_ty_value	check_associated_ty_value	115 tests
check_coherence	check_coherence	131 tests
check_crate	check crate	131 tests
check_crate_item	free fn	94 tests
check_crate_item	trait	131 tests
check_crate_item	trait impl	127 tests
check_drop_impl_always_applicable	not a Drop impl	127 tests
check_fn	check fn	96 tests
check_fn_body	trusted fn body	12 tests
check_free_fn	check free fn	94 tests
check_safety_matches	safety matches	127 tests
check_trait	check trait	131 tests
check_trait_impl	check_trait_impl	127 tests
check_trait_impl_item	associated ty value	115 tests
check_trait_item	associated ty in trait	116 tests
is_local_trait_ref	local trait	126 tests
orphan_check	orphan_check	127 tests
`overlap_check`	`not_goal`	115 tests (not in the report)
`overlap_check`	`skip_different_trait`	115 tests (not in the report)
`overlap_check`	`skip_same_impl`	127 tests (not in the report)
prove_after	prove_after	154 tests
prove_eq	existential	141 tests
prove_eq	rigid	119 tests
prove_eq	symmetric	138 tests
prove_existential_var_eq	existential-universal	132 tests
`prove_outlives`	`outlive through assumption`	113 tests (not in the report)
prove_wc	eq	148 tests
prove_wc	outlives	113 tests
prove_wc	parameter well formed	121 tests
prove_wc	positive impl	136 tests
prove_wc	trait ref is local	128 tests
prove_wc_list	none	155 tests
prove_wc_list	some	154 tests
prove_wf	tuples	36 tests
prove_wf	universal variables	124 tests

Premises failed (0)

This test records no negative coverage.

Proof trees

Proof tree

check_all_crates (check all prefixes) mod.rs:54
- args
- for_all mod.rs:41
  - for_all mod.rs:51
    
    args
    
    check_crate (check crate) mod.rs:75
    
    args
    
    for_all mod.rs:60
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait) mod.rs:188
    
    args
    
    check_trait (check trait) traits.rs:26
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:85
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:340
    
    args
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait impl) mod.rs:195
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:41
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (positive impl) prove_wc.rs:81
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (eq) prove_wc.rs:120
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args

… (200 of 1065 nodes shown)

Keyboard shortcuts

A MIR Formality

Test tests/functions.rs:25

Rules proved (37)

Premises failed (0)

Proof trees

Test `tests/functions.rs:25`