Test `foo`

Source location: tests/return_validation.rs:118

fn foo() -> u32 {
    'a: loop {
        break 'a;
    }
    return 0_u32;
}

Rules proved (53)

Judgment	Rule	All tests of this rule
borrow_check	borrow_check	175 tests
borrow_check_block	basic block	175 tests
borrow_check_expr	literal	114 tests
borrow_check_loop	fixed-point	23 tests
borrow_check_loop	loop	20 tests
borrow_check_statement	break	17 tests
borrow_check_statement	loop	23 tests
borrow_check_statement	return	79 tests
check_all_crates	check all prefixes	214 tests
check_associated_ty	check associated ty	195 tests
check_associated_ty_value	check_associated_ty_value	194 tests
check_coherence	check_coherence	214 tests
check_crate	check crate	214 tests
check_crate_item	free fn	175 tests
check_crate_item	trait	214 tests
check_crate_item	trait impl	210 tests
check_drop_impl_always_applicable	not a Drop impl	210 tests
check_fn	check fn	200 tests
check_fn_body	expr fn body	175 tests
check_fn_body	no fn body	192 tests
check_fn_in_trait	check fn in trait	193 tests
check_free_fn	check free fn	175 tests
check_safety_matches	safety matches	210 tests
check_trait	check trait	214 tests
check_trait_impl	check_trait_impl	210 tests
check_trait_impl_item	associated ty value	194 tests
check_trait_item	associated ty in trait	195 tests
check_trait_item	fn in trait	193 tests
drop_places	drop_places	175 tests
is_local_trait_ref	local trait	205 tests
orphan_check	orphan_check	210 tests
overlap_check_impl	different trait	194 tests
overlap_check_impl	not goal	195 tests
overlap_check_impl	same impl	210 tests
prove_after	prove_after	237 tests
prove_assignable	subtype	129 tests
prove_eq	existential	223 tests
prove_eq	rigid	201 tests
prove_eq	symmetric	220 tests
prove_existential_var_eq	existential-universal	214 tests
prove_outlives	outlive through assumption	195 tests
prove_predicate	eq	231 tests
prove_predicate	outlives	195 tests
prove_predicate	parameter well formed	204 tests
prove_predicate	positive impl	219 tests
prove_predicate	subtype	134 tests
prove_predicate	trait ref is local	211 tests
prove_predicate_list	none	238 tests
prove_predicate_list	some	237 tests
prove_wf	integers and booleans	131 tests
prove_wf	references	192 tests
prove_wf	tuples	200 tests
prove_wf	universal variables	206 tests

Premises failed (0)

This test records no negative coverage.

Proof trees

Proof tree

check_all_crates (check all prefixes) mod.rs:55
- args
- for_all mod.rs:42
  - for_all mod.rs:52
    
    args
    
    check_crate (check crate) mod.rs:76
    
    args
    
    for_all mod.rs:61
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait) mod.rs:189
    
    args
    
    check_trait (check trait) traits.rs:25
    
    args
    
    scope traits.rs:9
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    check_safety_matches (safety matches) impls.rs:83
    
    args
    
    check_drop_impl_always_applicable (not a Drop impl) impls.rs:342
    
    args
    
    for_all mod.rs:73
    
    args
    
    check_crate_item (trait impl) mod.rs:196
    
    args
    
    check_trait_impl (check_trait_impl) impls.rs:40
    
    args
    
    scope impls.rs:14
    
    prove_predicate_list (none) prove_predicate_list.rs:21
    
    args
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (positive impl) prove_predicate.rs:79
    
    args
    
    scope prove_predicate.rs:22
    
    prove_predicate_list (some) prove_predicate_list.rs:28
    
    args
    
    prove_predicate (eq) prove_predicate.rs:116
    
    args

… (200 of 3400 nodes shown)

How to read this page

Keyboard shortcuts

A MIR Formality

Test foo

Rules proved (53)

Premises failed (0)

Proof trees

Test `foo`