Test `main`

Source location: tests/codegen.rs:1102

fn main() -> () {
    let p: Pair = Pair { a: 1_u32, b: 10_u32 };
    p.b += p.a;
    println!(p.b);
}

Rules proved (66)

Judgment	Rule	All tests of this rule
access_kind_for_place_use	move	100 tests
access_permitted	access_permitted	103 tests
access_permitted_by_loans	access_permitted_by_loans	106 tests
borrow_check	borrow_check	175 tests
borrow_check_block	basic block	175 tests
borrow_check_expr	assign-op	7 tests
borrow_check_expr	literal	114 tests
borrow_check_expr	place	100 tests
borrow_check_expr	struct	19 tests
borrow_check_expr_has_ty	block	118 tests
borrow_check_place_expr	local	103 tests
borrow_check_place_expr	struct field	19 tests
borrow_check_statement	expr	47 tests
borrow_check_statement	let	94 tests
borrow_check_statement	print	75 tests
check_adt	check adt	59 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	adt	59 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_place_is_movable	field	7 tests
prove_place_is_movable	local	89 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_ty_is_rigid	rigid	76 tests
prove_wf	ADT	46 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 3472 nodes shown)

How to read this page

Keyboard shortcuts

A MIR Formality

Test main

Rules proved (66)

Premises failed (0)

Proof trees

Test `main`