Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Coverage report

Judgment/RulePositive coverageNegative coverage
fmt--
all_even--
↳ all_even2 tests0/1
sum_all--
↳ sum2 tests0/1
transitive_reachable--
↳ base2 tests0/1
↳ transitive2 tests0/2
is_zero--
↳ is_zero✗0/1
is_one--
↳ is_one✗N/A
prove_thing--
↳ positive✗0/1
↳ zero✗0/1
only_one--
↳ one✗0/1
mixed--
↳ kitchen sink✗0/3
↳ fallible let✗0/1
↳ all infallible✗N/A
move_place--
↳ copy✗0/2
↳ give✗0/1
check_adt--
↳ check adt45 tests2/3
borrow_check--
↳ borrow_check90 tests1/1
borrow_check_block--
↳ basic block90 tests1/3
borrow_check_statement-no applicable rule observed
↳ let70 tests1/3
↳ if28 tests2/3
↳ expr25 tests1/1
↳ loop22 tests1/2
↳ break17 tests1/2
↳ continue3 tests2/3
↳ return64 tests2/3
↳ block6 tests1/1
↳ exists36 tests1/2
↳ exists36 tests2/3
↳ exists36 tests2/3
↳ print24 tests0/1
borrow_check_expr_has_ty--
↳ block72 tests2/2
borrow_check_expr--
↳ assign22 tests3/4
↳ call25 tests3/8
↳ literal55 testsN/A
↳ true27 testsN/A
↳ false6 testsN/A
↳ ref29 tests2/3
↳ place71 tests3/4
↳ fn-name7 tests2/4
↳ turbofish19 tests1/2
↳ struct12 tests1/6
borrow_check_loop--
↳ loop20 tests2/2
↳ fixed-point22 tests2/2
borrow_check_place_expr--
↳ local73 tests1/1
↳ struct field12 tests2/7
↳ tuple field✗0/4
↳ parens7 tests0/1
↳ deref-ref30 tests0/2
drop_places--
↳ drop_places90 tests0/1
access_permitted--
↳ access_permitted73 tests2/2
access_permitted_by_loans--
↳ access_permitted_by_loans76 tests0/1
access_permitted_by_loan--
↳ borrow of disjoint places29 tests1/1
↳ read-shared is ok✗N/A
↳ write-indirect9 tests2/4
↳ loan is dead15 tests1/3
access_kind_for_place_use--
↳ copy✗0/1
↳ move71 testsN/A
prove_ty_is_copy--
↳ trait9 tests1/1
prove_place_is_movable--
↳ local68 testsN/A
↳ field3 tests1/2
↳ copy9 tests1/1
prove_ty_is_ref--
↳ ref9 tests0/1
prove_ty_is_rigid--
↳ rigid33 testsN/A
↳ normalize7 tests0/2
prove_assignable--
↳ never-to-b✗0/1
↳ subtype82 tests1/1
loan_cannot_outlive_universal_regions--
↳ loan_not_required_by_universal_regions15 tests1/1
loan_not_required_by_live_places--
↳ loan_not_required_by_live_places15 tests0/1
loan_not_required_by_live_place--
↳ loan is not required by type10 tests1/2
loan_not_required_by_live_place_prefix--
↳ no prefix10 tests0/1
↳ prefix3 tests0/2
loan_not_required_by_parameter--
↳ rigid-ty10 tests1/1
↳ alias-ty RFC 12143 tests1/1
↳ for-all-type✗0/1
↳ universal-variable✗1/1
↳ lifetime8 tests1/1
loan_cannot_outlive--
↳ loan_cannot_outlive8 tests1/1
loan_not_required_by_parameters--
↳ loan_not_required_by_parameters10 tests0/1
verify_universal_outlives--
↳ verify_universal_outlives32 tests0/1
only_assumed_outlives--
↳ existential31 tests0/1
↳ universal lifetime24 tests0/2
can_outlive--
↳ existential target19 tests0/1
↳ universal target3 tests1/3
check_coherence--
↳ check_coherence131 tests0/3
orphan_check--
↳ orphan_check127 tests1/1
orphan_check_neg--
↳ orphan_check_neg3 tests1/1
overlap_check_impl--
↳ same impl127 tests1/1
↳ different trait115 tests1/1
↳ not goal115 tests1/3
↳ inverted1 test2/4
check_free_fn--
↳ check free fn94 tests1/1
check_fn--
↳ check fn96 tests1/4
check_fn_body--
↳ no fn body1 testN/A
↳ trusted fn body12 testsN/A
↳ expr fn body90 tests1/2
check_trait_impl--
↳ check_trait_impl127 tests5/9
check_neg_trait_impl--
↳ check_neg_trait_impl3 tests1/1
↳ check_neg_trait_impl3 tests1/4
check_safety_matches--
↳ safety matches127 tests1/1
check_trait_impl_item--
↳ fn in impl✗0/1
↳ associated ty value115 tests0/1
check_fn_in_impl--
↳ check_fn_in_impl✗0/7
check_associated_ty_value--
↳ check_associated_ty_value115 tests0/6
check_drop_impl_always_applicable--
↳ not a Drop impl127 tests0/1
↳ Drop impl is always applicable6 tests3/6
check_all_crates--
↳ check all prefixes131 tests0/1
check_crate--
↳ check crate131 tests3/4
check_crate_item--
↳ trait131 tests1/1
↳ trait impl127 tests2/2
↳ adt45 tests1/1
↳ free fn94 tests1/1
↳ neg trait impl3 tests1/1
↳ test✗0/1
↳ feature gate45 testsN/A
check_trait--
↳ check trait131 tests2/3
check_trait_item--
↳ fn in trait2 tests0/1
↳ associated ty in trait116 tests0/1
check_fn_in_trait--
↳ check fn in trait2 tests0/1
check_associated_ty--
↳ check associated ty116 tests0/1
codegen_function--
↳ function✗0/3
codegen_block--
↳ block✗0/2
↳ labeled-block✗0/2
codegen_stmt--
↳ let-init✗0/3
↳ let-no-init✗0/2
↳ return✗0/1
↳ print✗0/4
↳ if✗0/3
↳ expr✗0/3
↳ loop✗0/3
↳ break✗0/1
↳ continue✗0/2
↳ block✗0/1
↳ exists✗0/2
codegen_expr_into--
↳ literal✗N/A
↳ fn-as-value✗0/2
↳ place✗0/2
↳ true✗N/A
↳ false✗N/A
↳ assign✗0/5
↳ turbofish✗N/A
↳ call✗0/7
↳ ref✗0/3
↳ struct✗0/4
resolve_place--
↳ resolve✗0/1
resolve_rigid--
↳ resolve✗0/1
type_expr--
↳ type_expr✗0/1
may_be_remote--
↳ may be defined downstream✗0/1
↳ may be added by upstream in a minor release✗0/1
may_be_downstream_trait_ref--
↳ may_be_downstream_trait_ref✗0/2
may_be_downstream_parameter--
↳ type variable✗N/A
↳ via normalize✗0/3
may_contain_downstream_type--
↳ existential variable✗N/A
↳ rigid type parameter✗0/2
↳ via normalize✗0/2
↳ forall✗0/1
normalizes_to_not_downstream--
↳ ambiguous✗0/2
is_local_trait_ref--
↳ local trait126 tests1/1
↳ local parameter11 tests2/3
is_not_downstream--
↳ lifetime✗N/A
↳ rigid2 testsN/A
↳ via normalize1 test1/2
↳ type variable✗N/A
is_local_parameter--
↳ local parameter1 test2/2
↳ fundamental rigid type✗1/2
↳ local rigid type10 tests1/1
↳ existential variable1 testN/A
prove_after--
↳ prove_after154 tests1/1
prove_const_has_type-no applicable rule observed
↳ rigid constant3 testsN/A
↳ block✗0/1
prove_eq--
↳ symmetric138 tests1/1
↳ rigid119 tests1/2
↳ alias1 test1/2
↳ existential141 tests1/1
↳ normalize-l19 tests2/2
prove_existential_var_eq--
↳ existential-nonvar43 tests2/2
↳ existential-existential12 testsN/A
↳ existential-universal132 tests1/1
prove_normalize-no applicable rule observed
↳ normalize-via-assumption4 tests1/2
↳ normalize-via-impl39 tests1/5
prove_normalize_via-no applicable rule observed
↳ var-axiom-l✗0/2
↳ var-axiom-r✗0/2
↳ axiom-l3 tests1/3
↳ axiom-r1 test0/3
↳ forall✗0/2
↳ implies✗0/2
prove_syntactically_eq--
↳ symmetric1 test1/1
↳ rigid✗0/2
↳ alias1 test1/2
↳ existential-nonvar1 test1/1
main--
↳ static outlives everything✗N/A
↳ anything outlives erased✗N/A
↳ erased outlives static✗N/A
↳ rigid types✗0/1
↳ outlive through assumption✗0/1
↳ anything can be pending✗0/1
prove_sub--
↳ normalize-l25 tests1/2
↳ normalize-r4 tests1/2
↳ rigid31 tests0/2
↳ lifetime => outlives28 tests0/1
prove_via-no applicable rule observed
↳ predicate-congruence-axiom13 tests1/3
↳ relation-axiom7 tests0/3
↳ forall2 tests1/1
↳ implies✗0/2
prove_wc--
↳ forall12 tests1/1
↳ implies4 tests1/1
↳ assumption19 tests1/2
↳ positive impl136 tests3/4
↳ coherence / remote impl✗0/2
↳ negative impl3 tests1/3
↳ alias eq1 test0/1
↳ trait implied bound1 test3/3
↳ eq148 tests1/1
↳ subtype82 tests1/1
↳ trait well formed19 tests2/2
↳ trait ref is local128 tests1/1
↳ outlives113 tests1/1
↳ parameter well formed121 tests1/1
↳ const has ty3 tests2/2
prove_wc_list--
↳ none155 testsN/A
↳ some154 tests2/2
prove_wf--
↳ universal variables124 testsN/A
↳ references41 tests1/3
↳ raw-pointers✗0/2
↳ tuples36 tests0/1
↳ integers and booleans97 tests0/1
↳ ADT32 tests1/3
↳ static lifetime1 testN/A
↳ scalar constants are always wf3 testsN/A
↳ aliases1 test0/1