Test next
Source location: tests/borrowck.rs:4356
fn next<'s>(f: &'s mut Filter) -> &'s mut u32 {
exists<'r0, 'r1, 'r2> {
'l: loop {
let item: &'r0 mut u32 = iter_next::<'r0>(&'r0 mut (*f).iter);
if true {
let keep: bool = call_predicate::<'r1, 'r2>(&'r1 mut (*f).predicate, &'r2 *item);
if keep {
return item;
} else {
}
} else {
break 'l;
}
}
return no_item::<'s>();
}
}
Rules proved (98)
Premises failed (32)
The last column links to the premise’s page when the judgment view counts this failure against that premise. It does not when the premise is read as infallible, or when the failure was blamed inside a multi-line premise that carries no record on its own first line.
| Judgment | Rule | Premise | All tests of this premise |
|---|---|---|---|
| borrow_check | borrow_check | borrow_check_block(env, assumptions, state, bloc… (line 138) | 60 tests |
| borrow_check_block | basic block | for_all(i in 0..stmts.len()) with(env, state) (b… (line 159, blamed at line 160) | not counted by the judgment view |
| borrow_check_statement | let | for_all(init in init.into_iter()) with (state) /… (line 192, blamed at line 194) | not counted by the judgment view |
| borrow_check_statement | loop | borrow_check_loop(env, assumptions, state, body,… (line 247) | 9 tests |
| borrow_check_statement | exists | borrow_check_block(env, assumptions_body, state,… (line 330) | 6 tests |
| borrow_check_expr_has_ty | block | borrow_check_expr(env, assumptions, state, expr,… (line 364) | 28 tests |
| borrow_check_expr | call | for_all(i in 0..args.len()) with(state) (borrow_… (line 442, blamed at line 443) | not counted by the judgment view |
| borrow_check_expr | ref | access_permitted( env, assumptions, state, Acces… (line 478) | 7 tests |
| borrow_check_loop | loop | borrow_check_block(env, assumptions, state, body… (line 587) | 9 tests |
| borrow_check_loop | loop | borrow_check_loop(env, assumptions, state, body,… (line 589) | 3 tests |
| borrow_check_loop | fixed-point | borrow_check_block(env, assumptions, state0, bod… (line 595) | 9 tests |
| borrow_check_loop | fixed-point | if state0 == state1 (line 596) | 3 tests |
| access_permitted | access_permitted | access_permitted_by_loans(env, assumptions, stat… (line 813) | 18 tests |
| access_permitted_by_loans | access_permitted_by_loans | for_all(loan in &state.current.loans_live) with(… (line 832, blamed at line 833) | not counted by the judgment view |
| access_permitted_by_loan | borrow of disjoint places | if place_disjoint_from_place(&loan.place, &acces… (line 855) | 23 tests |
| access_permitted_by_loan | write-indirect | if let TypedPlaceExpressionData::Deref(place_loa… (line 882) | 21 tests |
| access_permitted_by_loan | write-indirect | if place_accessed.is_prefix_of(place_loaned_ref) (line 884) | 7 tests |
| access_permitted_by_loan | loan is dead | loan_not_required_by_live_places(env, assumption… (line 902) | 23 tests |
| loan_cannot_outlive_universal_regions | loan_not_required_by_universal_regions | if outlived_by_loan.iter().all(|p| match p { // … (line 1197) | 5 tests |
| loan_not_required_by_live_places | loan_not_required_by_live_places | for_all(live_place in places_live_after_access) … (line 1249, blamed at line 1251) | not counted by the judgment view |
| loan_not_required_by_live_place | loan is not required by type | loan_not_required_by_parameter(env, assumptions,… (line 1278) | 23 tests |
| loan_not_required_by_parameter | rigid-ty | loan_not_required_by_parameters(env, assumptions… (line 1346) | 23 tests |
| loan_not_required_by_parameter | universal-variable | loan_cannot_outlive_universal_regions(env, assum… (line 1420) | 5 tests |
| loan_not_required_by_parameter | lifetime | loan_cannot_outlive(env, assumptions, outlives, … (line 1436) | 23 tests |
| loan_cannot_outlive | loan_cannot_outlive | if !outlived_by_loan.contains(&lifetime.upcast()… (line 1456) | 23 tests |
| loan_not_required_by_parameters | loan_not_required_by_parameters | for_all(param in live_parameters) (loan_not_requ… (line 1483, blamed at line 1484) | not counted by the judgment view |
| check_free_fn | check free fn | check_fn(program, Env::default(), Wcs::t(), f, c… (line 24) | 61 tests |
| check_fn | check fn | check_fn_body(program, env, assumptions, body, i… (line 55) | 60 tests |
| check_fn_body | expr fn body | borrow_check(typeck_env, assumptions, initial_st… (line 90) | 60 tests |
| check_all_crates | check all prefixes | for_all(i in 0..crates.len()) (let program = cra… (line 51, blamed at line 53) | not counted by the judgment view |
| check_crate | check crate | for_all(item in &c.items) (check_crate_item(prog… (line 72, blamed at line 73) | not counted by the judgment view |
| check_crate_item | free fn | check_free_fn(program, f, crate_id) => () (line 206) | 61 tests |
Proof trees
Proof tree
check_all_crates (check all prefixes)mod.rs:54args
for_allmod.rs:41for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
Failed proof tree
check_all_crates failedmod.rs:41args
rule "check all prefixes"mod.rs:53check_crate failedmod.rs:60args
rule "check crate"mod.rs:73check_crate_item failedmod.rs:178rule "free fn"mod.rs:206check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:55check_fn_body failedfns.rs:62args
rule "expr fn body"fns.rs:90borrow_check failednll.rs:127args
rule "borrow_check"nll.rs:138borrow_check_block failednll.rs:145rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "exists"nll.rs:330borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "loop"nll.rs:247borrow_check_loop failednll.rs:575args
rule "fixed-point"nll.rs:596 (failed: if_false)rule "loop"nll.rs:589borrow_check_loop failednll.rs:575args
rule "fixed-point"nll.rs:595borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "let"nll.rs:194borrow_check_expr_has_ty failednll.rs:351rule "block"nll.rs:364borrow_check_expr failednll.rs:372rule "call"nll.rs:443borrow_check_expr_has_ty failednll.rs:351rule "block"nll.rs:364borrow_check_expr failednll.rs:372rule "ref"nll.rs:478access_permitted failednll.rs:797rule "access_permitted"nll.rs:813access_permitted_by_loans failednll.rs:820rule "access_permitted_by_loans"nll.rs:833access_permitted_by_loan failednll.rs:840args
rule "borrow of disjoint places"nll.rs:855 (failed: if_false)rule "loan is dead"nll.rs:902loan_not_required_by_live_places failednll.rs:1226rule "loan_not_required_by_live_places"nll.rs:1251loan_not_required_by_live_place failednll.rs:1258args
rule "loan is not required by type"nll.rs:1278loan_not_required_by_parameter failednll.rs:1326args
rule "rigid-ty"nll.rs:1346loan_not_required_by_parameters failednll.rs:1463args
rule "loan_not_required_by_parameters"nll.rs:1484loan_not_required_by_parameter failednll.rs:1326args
rule "lifetime"nll.rs:1436loan_cannot_outlive failednll.rs:1443args
rule "loan_cannot_outlive"nll.rs:1456 (failed: if_false)
rule "universal-variable"nll.rs:1420loan_cannot_outlive_universal_regions failednll.rs:1170args
rule "loan_not_required_by_universal_regions"nll.rs:1197 (failed: if_false)
rule "write-indirect"nll.rs:882 (failed: if_let)rule "write-indirect"nll.rs:882 (failed: if_let)rule "write-indirect"nll.rs:884 (failed: if_false)
rule "loop"nll.rs:587borrow_check_block failednll.rs:145args
rule "basic block"nll.rs:160borrow_check_statement failednll.rs:177args
rule "let"nll.rs:194borrow_check_expr_has_ty failednll.rs:351rule "block"nll.rs:364borrow_check_expr failednll.rs:372rule "call"nll.rs:443borrow_check_expr_has_ty failednll.rs:351rule "block"nll.rs:364borrow_check_expr failednll.rs:372rule "ref"nll.rs:478access_permitted failednll.rs:797rule "access_permitted"nll.rs:813access_permitted_by_loans failednll.rs:820rule "access_permitted_by_loans"nll.rs:833access_permitted_by_loan failednll.rs:840args
rule "borrow of disjoint places"nll.rs:855 (failed: if_false)rule "loan is dead"nll.rs:902loan_not_required_by_live_places failednll.rs:1226rule "loan_not_required_by_live_places"nll.rs:1251loan_not_required_by_live_place failednll.rs:1258args
rule "loan is not required by type"nll.rs:1278loan_not_required_by_parameter failednll.rs:1326args
rule "rigid-ty"nll.rs:1346loan_not_required_by_parameters failednll.rs:1463args
rule "loan_not_required_by_parameters"nll.rs:1484loan_not_required_by_parameter failednll.rs:1326args
rule "lifetime"nll.rs:1436loan_cannot_outlive failednll.rs:1443args
rule "loan_cannot_outlive"nll.rs:1456 (failed: if_false)
rule "universal-variable"nll.rs:1420loan_cannot_outlive_universal_regions failednll.rs:1170args
rule "loan_not_required_by_universal_regions"nll.rs:1197 (failed: if_false)
rule "write-indirect"nll.rs:882 (failed: if_let)rule "write-indirect"nll.rs:882 (failed: if_let)rule "write-indirect"nll.rs:884 (failed: if_false)