Positive coverage: borrow_check_statement / loop
loop| Line | Coverage | Source |
|---|---|---|
| 247 | N/A | (let continue_live = Stmt::loop_(label, body).live_before(&env, &state, places_live_on_exit)) |
| 248 | ✗ | (let state = state.push_continue_scope(&env.env, label, places_live_on_exit, continue_live)?) |
| 249 | 9 | (borrow_check_loop(env, assumptions, state, body, places_live_on_exit) => state) |
| 250 | N/A | (let state = state.pop_scope(label)) |
| ──────── ("loop") | ||
| 252 | 23 | (borrow_check_statement(env, assumptions, state, Stmt::Loop { label, body }, places_live_on_exit) => (env, state)) |
23 tests exercised this rule:
Source location: tests/borrowck.rs:3156 (all coverage from this test)
fn foo() -> u32 {
exists<'r0, 'r1> {
'a: loop {
let x: i32 = 0_i32;
let r: &'r0 i32 = &'r1 x;
let _y: i32 = *r;
continue 'a;
}
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:4214 (all coverage from this test)
fn remove_last_node_iterative<'a>(node: &'a mut List) -> u32 {
exists<'r0, 'r1> {
let cursor: &'r0 mut List = &'r0 mut *node;
'l: loop {
let next: &'r1 mut List = &'r1 mut *cursor;
if true {
cursor = next;
} else {
break 'l;
}
}
*cursor = List { value: 0_u32 };
return 0_u32;
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:4276 (all coverage from this test)
fn no_control_flow() -> u32 {
exists<'r0, 'r1, 'r2, 'r3> {
let b: X = X { value: 0_u32 };
let p: &'r0 mut X = &'r1 mut b;
'l: loop {
let now: &'r2 mut X = &'r2 mut *p;
if true {
let next: &'r3 mut X = next_of::<'r3>(&'r3 mut *now);
p = next;
} else {
break 'l;
}
}
return 0_u32;
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:4326 (all coverage from this test)
fn conditional() -> u32 {
exists<'r0, 'r1, 'r2, 'r3> {
let b: X = X { value: 0_u32 };
let p: &'r0 mut X = &'r1 mut b;
'l: loop {
let now: &'r2 mut X = &'r2 mut *p;
if true {
if true {
let next: &'r3 mut X = next_of::<'r3>(&'r3 mut *now);
p = next;
} else {
}
} else {
break 'l;
}
}
return 0_u32;
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:4415 (all coverage from this test)
fn conditional_with_indirection() -> u32 {
exists<'r0, 'r1, 'r2, 'r3> {
let b: X = X { value: 0_u32 };
let p: &'r0 mut X = &'r1 mut b;
'l: loop {
let now: &'r2 mut X = &'r2 mut *p;
if true {
if true {
let next: &'r3 mut X = next_of::<'r3>(&'r3 mut *p);
p = next;
} else {
}
} else {
break 'l;
}
}
return 0_u32;
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:4467 (all coverage from this test)
fn to_refs<'a>(list: &'a mut List) -> &'a mut u32 {
exists<'r0, 'r1> {
let result: &'a mut u32;
'l: loop {
result = &'r0 mut (*list).value;
if true {
let n: &'r1 mut List = next_from_field::<'r1>(&'r1 mut (*list).next);
list = n;
} else {
return result;
}
}
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:4502 (all coverage from this test)
fn to_refs2<'a>(list: &'a mut List) -> &'a mut u32 {
exists<'r0, 'r1> {
let result: &'a mut u32;
'l: loop {
result = &'r0 mut (*list).value;
if true {
let n: &'r1 mut List = next_from_field::<'r1>(&'r1 mut (*list).next);
list = n;
} else {
break 'l;
}
}
return result;
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:4549 (all coverage from this test)
fn to_refs3<'a>(list: &'a mut List) -> &'a mut u32 {
exists<'r0, 'r1> {
let result: &'a mut u32;
let cursor: &'a mut List = &'a mut *list;
'l: loop {
result = &'r0 mut (*cursor).value;
if true {
let n: &'r1 mut List = next_from_field::<'r1>(&'r1 mut (*cursor).next);
cursor = n;
} else {
return result;
}
}
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:4592 (all coverage from this test)
fn next<'a>(d: &'a mut Decoder) -> &'a u32 {
exists<'r0, 'r1> {
'l: loop {
let buf: &'r0 u32 = fill_buf::<'r0>(&'r0 mut (*d).buf_read);
let s: &'r1 u32 = decode::<'r1>(buf);
if true {
return s;
} else {
}
}
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:4715 (all coverage from this test)
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>();
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/codegen.rs:12 (all coverage from this test)
fn main() -> () {
'a: loop {}
}
Proof trees omitted for the remaining 13 tests; each one is on its test’s page in Coverage by test.
Source location: tests/codegen.rs:205 (all coverage from this test)
fn main() -> () {
let x: i32 = 0_i32;
'a: loop {
println!(x);
break 'a;
}
}
Source location: tests/codegen.rs:410 (all coverage from this test)
fn main() -> () {
let x: i32 = 0_i32;
'a: loop {
if true {
println!(x);
break 'a;
} else {
continue 'a;
}
}
}
Source location: tests/codegen.rs:428 (all coverage from this test)
fn main() -> () {
'outer: loop {
println!(1_i32);
'inner: loop {
println!(2_i32);
break 'outer;
}
}
println!(3_i32);
}
Source location: tests/codegen.rs:448 (all coverage from this test)
fn main() -> () {
'a: loop {
if true {
println!(1_i32);
break 'a;
} else {
println!(2_i32);
break 'a;
}
}
println!(3_i32);
}
Source location: tests/codegen.rs:469 (all coverage from this test)
fn main() -> () {
let x: i32 = 0_i32;
'a: loop {
if false {
x = 1_i32;
break 'a;
} else {
x = 2_i32;
break 'a;
}
}
println!(x);
}
Source location: tests/codegen.rs:532 (all coverage from this test)
fn main() -> () {
let x: i32 = 0_i32;
'a: loop {
x = 77_i32;
break 'a;
}
println!(x);
}
Source location: tests/codegen.rs:550 (all coverage from this test)
fn main() -> () {
let x: i32 = 0_i32;
'a: loop {
{
x = 88_i32;
break 'a;
}
}
println!(x);
}
Source location: tests/mir_typeck.rs:110 (all coverage from this test)
fn foo() -> u32 {
let v0: u32 = 0_u32;
loop {
v0 = v0;
}
}
Source location: tests/mir_typeck.rs:1014 (all coverage from this test)
fn foo() -> u32 {
'a: loop {
break 'a;
}
return 0_u32;
}
Source location: tests/mir_typeck.rs:1073 (all coverage from this test)
fn foo() -> u32 {
'a: loop {
continue 'a;
}
return 0_u32;
}
Source location: tests/return_validation.rs:84 (all coverage from this test)
fn foo() -> u32 {
loop {
}
}
Source location: tests/return_validation.rs:118 (all coverage from this test)
fn foo() -> u32 {
'a: loop {
break 'a;
}
return 0_u32;
}