Positive coverage: borrow_check_place_expr / parens
parens| Line | Coverage | Source |
|---|---|---|
| 715 | ✗ | (borrow_check_place_expr(env, assumptions, state, place) => (place_typed, state)) |
| ──────── ("parens") | ||
| 717 | 8 | (borrow_check_place_expr(env, assumptions, state, PlaceExpr::Parens(place)) => (place_typed, state)) |
8 tests exercised this rule:
Source location: tests/borrowck.rs:2827 (all coverage from this test)
fn min_problem_case_4<'a>(list: &'a mut Map, list2: &'a mut Map) -> u32 {
exists<'r0> {
let num: &'r0 mut u32 = &'r0 mut (*list).value;
list = &'a mut *list2;
num;
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:391 (all coverage from this test)
fn main() -> () {
let p: Pair = Pair { x: 10_i32, y: 20_i32 };
exists<'a> {
let r: & 'a Pair = & 'a p;
println!((*r).x);
println!((*r).y);
}
}
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/mir_typeck.rs:1142 (all coverage from this test)
fn foo<'a>(v1: &'a Pair) -> u32 {
exists<'r0> {
let v2: u32 = (*v1).value;
return v2;
}
}
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