Positive coverage: check_associated_ty / check associated ty
check associated ty| Line | Coverage | Source |
|---|---|---|
| 84 | N/A | (let AssociatedTy { id: _, binder } = associated_ty) |
| 85 | N/A | (let (env, bound_data) = env.instantiate_universally(binder)) |
| 86 | N/A | (let AssociatedTyBoundData { ensures: _, where_clauses } = bound_data) |
| 89 | ✗ | (super::where_clauses::prove_where_clauses_well_formed( program, env, (trait_where_clauses, where_clauses), where_clauses, ) => ()) |
| ──────── ("check associated ty") | ||
| 94 | 99 | (check_associated_ty(program, env, trait_where_clauses, associated_ty) => ()) |
99 tests exercised this rule:
Source location: tests/basic_tests.rs:58
#[test]
fn hello_world() {
FormalityTest::new(crates![crate Foo {
trait Foo<T> where T: Bar<Self>, Self: Baz {}
trait Bar<T> where T: Baz {}
trait Baz {}
impl Baz for u32 {}
impl Bar<u32> for u32 {}
impl<T> Bar<T> for () where T: Baz {}
}])
.skip_execute()
.ok()
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54for_allmod.rs:41for_allmod.rs:51check_crate (check crate)mod.rs:75for_allmod.rs:60for_allmod.rs:72check_crate_item (trait)mod.rs:173check_trait (check trait)traits.rs:26prove_wc_list (none)prove_wc_list.rs:24
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20
Source location: tests/borrowck.rs:113
fn foo() -> Datum {
let x: Datum = Datum { value: 0 _ u32 };
let y: Datum = x;
x = Datum { value: 1 _ u32 };
let z: Datum = x;
return z;
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54for_allmod.rs:41for_allmod.rs:51check_crate (check crate)mod.rs:75for_allmod.rs:60for_allmod.rs:72check_crate_item (trait)mod.rs:173check_trait (check trait)traits.rs:26prove_wc_list (none)prove_wc_list.rs:24
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20
Source location: tests/borrowck.rs:186
fn foo() -> u32 {
let x: u32;
if true {
x = 1 _ u32;
} else {
x = 2 _ u32;
}
return x;
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54for_allmod.rs:41for_allmod.rs:51check_crate (check crate)mod.rs:75for_allmod.rs:60for_allmod.rs:72check_crate_item (trait)mod.rs:173check_trait (check trait)traits.rs:26prove_wc_list (none)prove_wc_list.rs:24
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20
Source location: tests/borrowck.rs:253
fn foo() -> Datum {
let x: Pair = Pair { first: Datum { value: 1 _ u32 }, second: Datum { value: 2 _ u32 } };
let a: Datum = x.first;
let b: Datum = x.second;
return b;
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54for_allmod.rs:41for_allmod.rs:51check_crate (check crate)mod.rs:75for_allmod.rs:60for_allmod.rs:72check_crate_item (trait)mod.rs:173check_trait (check trait)traits.rs:26prove_wc_list (none)prove_wc_list.rs:24
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20
Source location: tests/borrowck.rs:1968
fn min_problem_case_3<'a>(m: &mut 'a Map) -> &mut 'a Map {
exists<'r0, 'r1> {
let n: &mut 'r0 Map = &mut 'r0 *m;
if true {
return n;
} else {
let o: &mut 'r1 Map = &mut 'r1 *m;
return o;
}
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54for_allmod.rs:41for_allmod.rs:51check_crate (check crate)mod.rs:75for_allmod.rs:60for_allmod.rs:72check_crate_item (trait)mod.rs:173check_trait (check trait)traits.rs:26prove_wc_list (none)prove_wc_list.rs:24
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20
Source location: tests/borrowck.rs:2041
fn foo() -> i32 {
exists<'r0, 'r1> {
let result: i32;
{
let v1: i32 = 22 _ i32;
let v2: &'r0 i32 = &'r1 v1;
result = *v2;
}
return result;
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54for_allmod.rs:41for_allmod.rs:51check_crate (check crate)mod.rs:75for_allmod.rs:60for_allmod.rs:72check_crate_item (trait)mod.rs:173check_trait (check trait)traits.rs:26prove_wc_list (none)prove_wc_list.rs:24
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20
Source location: tests/borrowck.rs:2156
fn min_problem_case_3<'a>(m: &mut 'a Map) -> &mut 'a Map {
exists<'r0, 'r1> {
let n: &mut 'r0 Map = &mut 'r0 *m;
if true {
} else {
}
let o: &mut 'r1 Map = &mut 'r1 *m;
return o;
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54for_allmod.rs:41for_allmod.rs:51check_crate (check crate)mod.rs:75for_allmod.rs:60for_allmod.rs:72check_crate_item (trait)mod.rs:173check_trait (check trait)traits.rs:26prove_wc_list (none)prove_wc_list.rs:24
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20
Source location: tests/borrowck.rs:2218
fn foo<'a, 'b>(v1: &'a u32) -> &'b u32
where
'a: 'b,
{
exists<'r0> {
let v2: &'r0 u32 = v1;
return v2;
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54for_allmod.rs:41for_allmod.rs:51check_crate (check crate)mod.rs:75for_allmod.rs:60for_allmod.rs:72check_crate_item (trait)mod.rs:173check_trait (check trait)traits.rs:26prove_wc_list (none)prove_wc_list.rs:24
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20
Source location: tests/borrowck.rs:2235
fn foo<'a, 'b, 'c>(v1: &'a u32) -> &'c u32
where
'a: 'b,
'b: 'c,
{
return v1;
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54for_allmod.rs:41for_allmod.rs:51check_crate (check crate)mod.rs:75for_allmod.rs:60for_allmod.rs:72check_crate_item (trait)mod.rs:173check_trait (check trait)traits.rs:26prove_wc_list (none)prove_wc_list.rs:24
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20
Source location: tests/borrowck.rs:2277
fn min_problem_case_4<'a>(list: &mut 'a Map, list2: &mut 'a Map) -> u32 {
exists<'r0> {
let num: &mut 'r0 u32 = &mut 'r0 (*list).value;
list = &mut 'a *list2;
num;
return 0 _ u32;
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54for_allmod.rs:41for_allmod.rs:51check_crate (check crate)mod.rs:75for_allmod.rs:60for_allmod.rs:72check_crate_item (trait)mod.rs:173check_trait (check trait)traits.rs:26prove_wc_list (none)prove_wc_list.rs:24
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_safety_matches (safety matches)impls.rs:79
check_drop_impl_always_applicable (not a Drop impl)impls.rs:295
for_allmod.rs:72check_crate_item (trait impl)mod.rs:180check_trait_impl (check_trait_impl)impls.rs:39prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (positive impl)prove_wc.rs:89prove_wc_list (some)prove_wc_list.rs:31prove_wc (eq)prove_wc.rs:128prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
prove_after (prove_after)prove_after.rs:20
Source location: tests/borrowck.rs:2410
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: &mut 'l_q u32 = &mut 'loan_0 a;
let p: &mut 'l_p u32 = &mut 'loan_1 a;
if true {
p = &mut 'loan_1 a;
q = &mut 'loan_2 b;
} else {
p = &mut 'loan_3 b;
}
*q = 1 _ u32;
return *p;
}
}
Proof trees omitted for the remaining 89 tests.
Source location: tests/borrowck.rs:2600
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;
}
}
}
Source location: tests/borrowck.rs:2628
fn foo() -> () {
'a: {
{
let 'a: v: i32 = 0 _ i32;
}
}
}
Source location: tests/borrowck.rs:2733
fn foo<'a>(m: &mut 'a Map) -> &mut 'a Map {
exists<'r0, 'r1> {
let n: &mut 'r0 Map = &mut 'r0 *m;
if false {
return n;
} else {
let o: &mut 'r1 Map = &mut 'r1 *m;
return o;
}
}
}
Source location: tests/borrowck.rs:2806
fn foo<'a>(a: &'a u32) -> &'a u32 {
exists<'r0> {
let r: &'r0 u32 = identity::<&'r0 u32>(a);
return r;
}
}
Source location: tests/borrowck.rs:2828
fn bar() -> u32 {
exists<'r1> {
let v: u32 = 7 _ u32;
let r: u32 = foo::<'r1>(&'r1 v);
return r;
}
}
Source location: tests/borrowck.rs:2856
fn foo<'a, 'b>(a: &'a u32) -> &'b u32
where 'a: 'b {
let r: &'b u32 = identity::<&'b u32>(a);
return r;
}
Source location: tests/borrowck.rs:2901
fn foo<'b>(a: &'b u32) -> &'b u32 {
let r: &'b u32 = bar::<'b, &'b u32>(a);
return r;
}
Source location: tests/borrowck.rs:2922
fn bar() -> u32 {
exists<'r0, 'r1> {
let v: u32 = 1 _ u32;
let p: &'r0 u32 = &'r1 v;
foo(0 _ u32);
return *p;
}
}
Source location: tests/borrowck.rs:2976
fn foo() -> u32 {
exists<'r0, 'r1, 'r2, 'r3> {
let p: Point = Point { x: 0 _ u32, y: 0 _ u32 };
let b1: &mut 'r0 u32 = &mut 'r1 p.x;
let b2: &mut 'r2 u32 = &mut 'r3 p.y;
*b1 = 1 _ u32;
*b2 = 2 _ u32;
return 0 _ u32;
}
}
Source location: tests/borrowck.rs:3095
fn reborrow<'a>(a: &mut 'a u8) -> &mut 'a u8 {
exists<'r0, 'r1, 'r2, 'r3> {
if true {
let b: &mut 'r1 u8 = &mut 'r0 *a;
return b;
} else { }
let c: &mut 'r3 u8 = &mut 'r2 *a;
return c;
}
}
Source location: tests/borrowck.rs:3120
fn reborrow<'a>(a: &mut 'a u8) -> &mut 'a u8 {
exists<'r0, 'r1, 'r2, 'r3> {
// This creates an outlives constraint
let b: &mut 'r1 u8 = &mut 'r0 *a;
if true {
return b;
} else {
// this means the loan remains live
}
// If the outlives constraint propagated here,
// we would get an error.
let c: &mut 'r3 u8 = &mut 'r2 *a;
return c;
}
}
Source location: tests/borrowck.rs:3137
fn reborrow<'a>(a: &mut 'a u8) -> &mut 'a u8 {
exists<'r0, 'r1, 'r2, 'r3> {
let b: &mut 'r1 u8 = &mut 'r0 *a;
return b;
let c: &mut 'r3 u8 = &mut 'r2 *a;
return c;
}
}
Source location: tests/borrowck.rs:3157
fn reborrow<'a>(a: &mut 'a u8) -> &mut 'a u8 {
exists<'r0, 'r1, 'r2, 'r3> {
if true {
let b: &mut 'r1 u8 = &mut 'r0 *a;
return b;
} else {
let c: &mut 'r3 u8 = &mut 'r2 *a;
return c;
}
}
}
Source location: tests/borrowck.rs:3225
fn foo() -> u32 {
exists<'r0, 'r1, 'r2> {
let x: u32 = 22 _ u32;
let p: &'r1 u32 = &'r0 x;
let q: &'r2 u32 = p;
x = 1 _ u32;
return 0 _ u32;
}
}
Source location: tests/codegen.rs:11
fn main() -> () {
println!(22 _ i32);
}
Source location: tests/codegen.rs:24
fn main() -> () {
println!(1 _ i32);
println!(true);
println!(false);
}
Source location: tests/codegen.rs:36
fn main() -> () {
let x: i32 = 42 _ i32;
println!(x);
}
Source location: tests/codegen.rs:49
fn main() -> () {
let x: i32 = 1 _ i32;
x = 2 _ i32;
println!(x);
}
Source location: tests/codegen.rs:64
fn main() -> () {
let y: i32 = add_one(1 _ i32);
println!(y);
}
Source location: tests/codegen.rs:79
fn main() -> () {
let y: i32 = identity::<i32>(42 _ i32);
println!(y);
}
Source location: tests/codegen.rs:95
fn main() -> () {
let x: i32 = 1 _ i32;
if true {
println!(x);
} else {
println!(0 _ i32);
}
}
Source location: tests/codegen.rs:110
fn main() -> () {
let x: i32 = 0 _ i32;
'a: loop {
println!(x);
break 'a;
}
}
Source location: tests/codegen.rs:127
fn main() -> () {
{
let x: i32 = 99 _ i32;
println!(x);
}
exists<'a> {
println!(1 _ i32);
}
}
Source location: tests/codegen.rs:141
fn main() -> () {
let p: Pair = Pair { x: 10 _ i32, y: 20 _ i32 };
println!(p.x);
println!(p.y);
}
Source location: tests/codegen.rs:171
fn main() -> () {
let a: usize = 100 _ usize;
let b: isize = 200 _ isize;
println!(a);
println!(b);
}
Source location: tests/codegen.rs:188
fn main() -> () {
let a: i32 = f(1 _ i32);
let b: i32 = f(2 _ i32);
let c: i32 = f(3 _ i32);
println!(a);
println!(b);
println!(c);
}
Source location: tests/codegen.rs:201
fn main() -> () {
let y: i32 = f(f(42 _ i32));
println!(y);
}
Source location: tests/codegen.rs:218
fn main() -> () {
let r: i32 = outer(7 _ i32);
println!(r);
}
Source location: tests/codegen.rs:238
fn main() -> () {
a();
}
Source location: tests/codegen.rs:251
fn main() -> () {
let r: i32 = first::<i32, bool>(10 _ i32, true);
println!(r);
}
Source location: tests/codegen.rs:264
fn main() -> () {
let w: Wrapper<i32> = Wrapper::<i32> { val: 42 _ i32 };
println!(w.val);
}
Source location: tests/codegen.rs:318
fn main() -> () {
let x: i32 = 0 _ i32;
'a: loop {
if true {
println!(x);
break 'a;
} else {
continue 'a;
}
}
}
Source location: tests/codegen.rs:336
fn main() -> () {
'outer: loop {
println!(1 _ i32);
'inner: loop {
println!(2 _ i32);
break 'outer;
}
}
println!(3 _ i32);
}
Source location: tests/codegen.rs:356
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:377
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:443
fn main() -> () {
let x: i32 = 0 _ i32;
'a: loop {
x = 77 _ i32;
break 'a;
}
println!(x);
}
Source location: tests/codegen.rs:461
fn main() -> () {
let x: i32 = 0 _ i32;
'a: loop {
{
x = 88 _ i32;
break 'a;
}
}
println!(x);
}
Source location: tests/codegen.rs:477
fn main() -> () {
'a: {
println!(1 _ i32);
break 'a;
println!(2 _ i32);
}
println!(3 _ i32);
}
Source location: tests/coherence_orphan.rs:84
#[test]
fn mirror_FooStruct() {
FormalityTest::new(crates![crate core {
trait CoreTrait {}
trait Mirror {
type Assoc : [];
}
impl<T> Mirror for T {
type Assoc = T;
}
},
crate foo {
struct FooStruct {}
impl CoreTrait for <FooStruct as Mirror>::Assoc {}
}])
.skip_execute()
.ok()
}
Source location: tests/coherence_orphan.rs:196
#[test]
fn CoreTraitLocal_for_AliasToKnown_in_Foo() {
// TODO: see comment in `orphan_check` from prev commit
FormalityTest::new(crates![crate core {
trait CoreTrait<T> {}
trait Unit {
type Assoc : [];
}
impl<T> Unit for T {
type Assoc = ();
}
},
crate foo {
struct FooStruct {}
impl CoreTrait<FooStruct> for <() as Unit>::Assoc {}
}])
.skip_execute()
.ok()
}
Source location: tests/coherence_overlap.rs:307
#[test]
fn is_local_unknowable_trait_ref() {
FormalityTest::new(crates![crate core {
trait Project {
type Assoc: [];
}
impl<T> Project for T {
type Assoc = T;
}
trait Foo<U> { }
},
crate foo {
struct LocalType {}
trait Overlap<U> {}
impl<T, U> Overlap<U> for T
where
<T as Project>::Assoc: Foo<U> {}
impl<T> Overlap<LocalType> for () {}
}])
.skip_execute()
.ok()
}
Source location: tests/const_generics_rv_tsv_parse.rs:11
#[test]
fn parse_minirust_22() {
FormalityTest::new(crates![crate Foo {
trait Trait<const N> where type_of_const N is usize {}
impl Trait<usize(22)> for u32 {}
}])
.skip_execute()
.ok()
}
Source location: tests/consts.rs:11
#[test]
fn nonsense_rigid_const_bound() {
FormalityTest::new(crates![crate Foo {
// This where-clause is not *provable*, but it is well-formed.
trait Foo where type_of_const true is u32 {}
}])
.skip_execute()
.ok()
}
Source location: tests/consts.rs:23
#[test]
fn ok() {
FormalityTest::new(crates![crate Foo {
trait Foo<const C> where type_of_const C is bool {}
trait Bar<const C> where type_of_const C is u32 {}
impl<const C> Foo<C> for u32 where type_of_const C is bool {}
}])
.skip_execute()
.ok()
}
Source location: tests/consts.rs:49
#[test]
fn holds() {
FormalityTest::new(crates![crate Foo {
trait Foo<const C> where type_of_const C is bool {}
impl Foo<true> for u32 {}
}])
.skip_execute()
.ok()
}
Source location: tests/consts.rs:58
#[test]
fn rigid_const_bound() {
FormalityTest::new(crates![crate Foo {
trait Foo where type_of_const true is bool {}
}])
.skip_execute()
.ok()
}
Source location: tests/consts.rs:92
#[test]
fn generic_match() {
FormalityTest::new(crates![crate Foo {
trait Foo<const C> where type_of_const C is bool {}
// Here, the impl matches the trait bound.
impl<const C> Foo<C> for u32 where type_of_const C is bool {}
}])
.skip_execute()
.ok()
}
Source location: tests/consts.rs:101
#[test]
fn multiple_type_of_const() {
FormalityTest::new(crates![crate Foo {
trait Foo<const C> where type_of_const C is bool, type_of_const C is u32 {}
}])
.skip_execute()
.ok()
}
Source location: tests/decl_safety.rs:12
#[test]
fn unsafe_trait() {
FormalityTest::new(crates![crate baguette {
unsafe trait Foo {}
unsafe impl Foo for u32 {}
}])
.skip_execute()
.ok()
}
Source location: tests/decl_safety.rs:22
#[test]
fn safe_trait() {
FormalityTest::new(crates![crate baguette {
safe trait Foo {}
safe impl Foo for u32 {}
}])
.skip_execute()
.ok()
}
Source location: tests/decl_safety.rs:32
#[test]
fn unsafe_trait_negative_impl() {
FormalityTest::new(crates![crate baguette {
unsafe trait Foo {}
impl !Foo for u32 {}
}])
.skip_execute()
.ok()
}
Source location: tests/drop.rs:20
#[test]
fn drop_impl_simple_struct() {
FormalityTest::new(crates![
crate Foo {
struct MyStruct {
value: u32,
}
impl Drop for MyStruct {}
}
])
.skip_execute()
.ok()
}
Source location: tests/drop.rs:38
#[test]
fn drop_impl_generic_struct() {
FormalityTest::new(crates![
crate Foo {
trait Clone {}
struct MyStruct<T> where T: Clone {
value: T,
}
impl<T> Drop for MyStruct<T> where T: Clone {}
}
])
.skip_execute()
.ok()
}
Source location: tests/drop.rs:54
#[test]
fn drop_impl_generic_no_where_clauses() {
FormalityTest::new(crates![
crate Foo {
struct Wrapper<T> {
value: T,
}
impl<T> Drop for Wrapper<T> {}
}
])
.skip_execute()
.ok()
}
Source location: tests/drop.rs:78
#[test]
fn drop_impl_subset_where_clauses() {
FormalityTest::new(crates![
crate Foo {
trait Clone {}
trait Debug {}
struct MyStruct<T> where T: Clone, T: Debug {
value: T,
}
// Impl has no where-clauses — but the struct requires them.
impl<T> Drop for MyStruct<T> {}
}
])
.skip_execute()
.ok()
}
Source location: tests/field_projections.rs:17
fn test(ptr: Ptr) -> () {
let x: () = *ptr;
}
Source location: tests/functions.rs:24
Source location: tests/functions.rs:37
Source location: tests/mir_typeck.rs:13
fn foo (v1: u32) -> u32 {
return v1;
}
Source location: tests/mir_typeck.rs:35
fn foo () -> u8 {
let v1: u16 = 5 _ u16;
let v2: u32 = 5 _ u32;
let v3: u64 = 5 _ u64;
let v4: usize = 5 _ usize;
let v5: i8 = 5 _ i8;
let v6: i16 = 5 _ i16;
let v7: i32 = 5 _ i32;
let v8: i64 = 5 _ i64;
let v9: isize = 5 _ isize;
let v10: bool = false;
return 5 _ u8;
}
Source location: tests/mir_typeck.rs:89
fn foo (v1: u32) -> u32 {
return v1;
}
Source location: tests/mir_typeck.rs:105
fn foo() -> u32 {
let v0: u32 = 0 _ u32;
loop {
v0 = v0;
}
}
Source location: tests/mir_typeck.rs:117
fn foo () -> bool {
return true;
}
Source location: tests/mir_typeck.rs:133
fn foo (b: bool) -> u32 {
if b {
return 1 _ u32;
} else {
return 2 _ u32;
}
}
Source location: tests/mir_typeck.rs:171
fn bar(v1: u32) -> u32 {
let v0: u32 = foo(v1);
return v0;
}
Source location: tests/mir_typeck.rs:191
fn foo (v1: u32) -> u32 {
return v1;
}
Source location: tests/mir_typeck.rs:234
fn foo (v1: u32) -> u32 {
let v2: Dummy = Dummy { value: 1 _ u32, is_true: false };
v2.value = 2 _ u32;
return v1;
}
Source location: tests/mir_typeck.rs:250
fn foo() -> () {
let s1: S1<u8>;
}
Source location: tests/mir_typeck.rs:345
fn bar(v1: u32) -> u32 {
let v0: u32 = identity::<u32>(v1);
return v0;
}
Source location: tests/mir_typeck.rs:670
fn foo() -> bool {
let v1: bool = false;
return v1;
}
Source location: tests/mir_typeck.rs:693
fn foo<'a>(v1: &'a u32) -> &'a u32 {
exists<'r0> {
let v2: &'r0 u32 = v1;
return v2;
}
}
Source location: tests/mir_typeck.rs:710
fn foo () -> u32 {
exists<'a> {
let v0: u32 = 0 _ u32;
let v1: &'a u32 = &'a v0;
let v2: u32 = *v1;
return v2;
}
}
Source location: tests/mir_typeck.rs:729
fn foo<'a, T>(v1: &'a T) -> T
where
T: Copy,
T: 'a,
{
exists<'r0> {
let v2: T = *v1;
return v2;
}
}
Source location: tests/mir_typeck.rs:755
fn foo() -> u32 {
'a: loop {
break 'a;
}
return 0 _ u32;
}
Source location: tests/mir_typeck.rs:802
fn foo() -> u32 {
'a: loop {
continue 'a;
}
return 0 _ u32;
}
Source location: tests/mir_typeck.rs:857
fn foo<'a>(v1: &'a Pair) -> u32 {
exists<'r0> {
let v2: u32 = (*v1).value;
return v2;
}
}
Source location: tests/mir_typeck.rs:882
fn foo() -> u32 {
'a: {
break 'a;
}
return 0 _ u32;
}
Source location: tests/return_validation.rs:31
fn foo() -> () {
}
Source location: tests/return_validation.rs:48
fn foo(b: bool) -> u32 {
if b {
return 1 _ u32;
} else {
return 2 _ u32;
}
}
Source location: tests/return_validation.rs:79
fn foo() -> u32 {
loop {
}
}
Source location: tests/return_validation.rs:111
fn foo() -> u32 {
'a: loop {
break 'a;
}
return 0 _ u32;
}
Source location: tests/return_validation.rs:124
fn foo() -> u32 {
return 42 _ u32;
}
Source location: tests/traits.rs:26
#[test]
fn trait_with_valid_associated_type() {
FormalityTest::new(crates![
crate core {
trait A {
type Assoc : [];
}
}
])
.skip_execute()
.ok();
}
Source location: tests/well_formed_struct.rs:17
fn main() -> () {
exists<'y> {
let a: u32 = 22 _ u32;
let f: Foo<'y> = Foo::<'y> { y: &'y a };
}
}
Source location: tests/well_formed_trait_ref.rs:19
#[test]
fn dependent_where_clause() {
FormalityTest::new(crates![crate foo {
trait Trait1 {}
trait Trait2 {}
struct S1<T> where T: Trait1 {
dummy: T,
}
struct S2<T> where T: Trait1, S1<T> : Trait2 {
dummy: T,
}
}])
.skip_execute()
.ok()
}
Source location: tests/well_formed_trait_ref.rs:56
#[test]
fn lifetime_param() {
FormalityTest::new(crates![crate foo {
trait Trait1<'a> {}
struct S1 {}
struct S2<'a> where S1: Trait1<'a> {}
}])
.skip_execute()
.ok()
}
Source location: tests/well_formed_trait_ref.rs:71
#[test]
fn static_lifetime_param() {
FormalityTest::new(crates![crate foo {
trait Trait1<'a> {}
struct S1 {}
impl Trait1<'static> for S1 {}
struct S2 where S1: Trait1<'static> {}
}])
.skip_execute()
.ok()
}
Source location: tests/well_formed_trait_ref.rs:86
#[test]
fn const_param() {
FormalityTest::new(crates![crate foo {
trait Trait1<const C> where type_of_const C is u32 {}
struct S1 {}
impl Trait1<u32(3)> for S1 {}
struct S2 where S1: Trait1<u32(3)> {}
}])
.skip_execute()
.ok()
}