Test `main`

Source location: tests/codegen.rs:251

fn main() -> () {
    let r: i32 = first::<i32, bool>(10_i32, true);
    println!(r);
}

Rules proved (58)

Judgment	Rule	All tests of this rule
access_kind_for_place_use	move	71 tests
access_permitted	access_permitted	73 tests
access_permitted_by_loans	access_permitted_by_loans	76 tests
borrow_check	borrow_check	90 tests
borrow_check_block	basic block	90 tests
borrow_check_expr	call	25 tests
borrow_check_expr	literal	55 tests
borrow_check_expr	place	71 tests
borrow_check_expr	true	27 tests
borrow_check_expr	turbofish	19 tests
borrow_check_expr_has_ty	block	72 tests
borrow_check_place_expr	local	73 tests
borrow_check_statement	let	70 tests
borrow_check_statement	print	24 tests
borrow_check_statement	return	64 tests
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	expr fn body	90 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
drop_places	drop_places	90 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_assignable	subtype	82 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_place_is_movable	local	68 tests
prove_ty_is_rigid	rigid	33 tests
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	subtype	82 tests
prove_wc	trait ref is local	128 tests
prove_wc_list	none	155 tests
prove_wc_list	some	154 tests
prove_wf	integers and booleans	97 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 1074 nodes shown)

Keyboard shortcuts

A MIR Formality

Test main

Rules proved (58)

Premises failed (0)

Proof trees

Test `main`