Test foo
Source location: tests/borrowck.rs:2635
fn foo () -> u32 {
exists<'l_p, 'l_q, 'loan_0, 'loan_1, 'loan_2, 'loan_3> {
let a: u32 = 0_u32;
let b: u32 = 0_u32;
// In Rustc, the 1-tuple is needed for some reason
// Niko does not 100% understand, else rustc is able to
// see that this program is safe.
let q: &'l_q mut u32 = &'loan_0 mut a;
let p: &'l_p mut u32 = &'loan_1 mut a;
if true {
p = &'loan_1 mut a;
q = &'loan_2 mut b;
} else {
p = &'loan_3 mut b;
}
*q = 1_u32;
return *p;
}
}
Rules proved (82)
Premises failed (0)
This test records no negative coverage.
Proof trees
Proof tree
check_all_crates (check all prefixes)mod.rs:54args
for_allmod.rs:41for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args