Positive coverage: check_crate_item / adt
adt| Line | Coverage | Source |
|---|---|---|
| 200 | 3 | (check_adt(program, &s.to_adt()) => ()) |
| ──────── ("adt") | ||
| 202 | 63 | (check_crate_item(program, CrateItem::AdtItem(s), crate_id) => ()) |
63 tests exercised this rule:
Source location: tests/basic_tests.rs:209
#[test]
fn non_lifetime_binder_in_enum_where_clause_pass() {
FormalityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }
trait B { }
enum E where for<U> u32: A<U> { }
impl <T> B for T {}
}])
.skip_execute()
.ok()
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54args
for_allmod.rs:41for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (feature gate)mod.rs:224args
for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (trait well formed)prove_wc.rs:141args
for_allcombinators.rs:69prove_wf (universal variables)prove_wf.rs:27args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (adt)mod.rs:201args
check_adt (check adt)adts.rs:27args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (forall)prove_wc.rs:36args
prove_wc (trait well formed)prove_wc.rs:141args
for_allcombinators.rs:69prove_wf (integers and booleans)prove_wf.rs:56args
for_allcombinators.rs:69prove_wf (universal variables)prove_wf.rs:27args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-universal)prove_eq.rs:141args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-universal)prove_eq.rs:141args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
check_coherence (check_coherence)coherence.rs:24args
for_allcoherence.rs:8for_allcoherence.rs:17args
for_allcoherence.rs:8for_allcoherence.rs:18args
overlap_check (skip_same_impl)coherence.rs:75
for_allcoherence.rs:8for_allcoherence.rs:20args
orphan_check (orphan_check)coherence.rs:39args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (trait ref is local)prove_wc.rs:147args
is_local_trait_ref (local trait)is_local.rs:208args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
Source location: tests/basic_tests.rs:239
#[test]
fn non_lifetime_binder_in_struct_where_clause_pass() {
FormalityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }
trait B { }
struct S<T> where for<U> u32: A<U> { }
impl <T> B for T {}
}])
.skip_execute()
.ok()
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54args
for_allmod.rs:41for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (feature gate)mod.rs:224args
for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (trait well formed)prove_wc.rs:141args
for_allcombinators.rs:69prove_wf (universal variables)prove_wf.rs:27args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (adt)mod.rs:201args
check_adt (check adt)adts.rs:27args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (forall)prove_wc.rs:36args
prove_wc (trait well formed)prove_wc.rs:141args
for_allcombinators.rs:69prove_wf (integers and booleans)prove_wf.rs:56args
for_allcombinators.rs:69prove_wf (universal variables)prove_wf.rs:27args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-universal)prove_eq.rs:141args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-universal)prove_eq.rs:141args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
check_coherence (check_coherence)coherence.rs:24args
for_allcoherence.rs:8for_allcoherence.rs:17args
for_allcoherence.rs:8for_allcoherence.rs:18args
overlap_check (skip_same_impl)coherence.rs:75
for_allcoherence.rs:8for_allcoherence.rs:20args
orphan_check (orphan_check)coherence.rs:39args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (trait ref is local)prove_wc.rs:147args
is_local_trait_ref (local trait)is_local.rs:208args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
Source location: tests/basic_tests.rs:426
Proof tree
check_all_crates (check all prefixes)mod.rs:54args
for_allmod.rs:41for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_alltraits.rs:9for_alltraits.rs:24args
check_trait_item (fn in trait)traits.rs:44args
check_fn_in_trait (check fn in trait)traits.rs:68args
check_fn (check fn)fns.rs:56prove_wc_list (none)prove_wc_list.rs:21args
for_allfns.rs:31for_allfns.rs:52args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (parameter well formed)prove_wc.rs:160args
prove_wf (integers and booleans)prove_wf.rs:56args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (parameter well formed)prove_wc.rs:160args
prove_wf (integers and booleans)prove_wf.rs:56args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_fn_body (trusted fn body)fns.rs:82args
for_allmod.rs:72args
check_crate_item (adt)mod.rs:201args
check_adt (check adt)adts.rs:27args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
check_coherence (check_coherence)coherence.rs:24args
for_allcoherence.rs:8for_allcoherence.rs:17args
for_allcoherence.rs:8for_allcoherence.rs:18args
overlap_check (skip_same_impl)coherence.rs:75
for_allcoherence.rs:8for_allcoherence.rs:20args
orphan_check (orphan_check)coherence.rs:39args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (trait ref is local)prove_wc.rs:147args
is_local_trait_ref (local trait)is_local.rs:208args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
Source location: tests/borrowck.rs:128
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:54args
for_allmod.rs:41for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
Source location: tests/borrowck.rs:270
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:54args
for_allmod.rs:41for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
Source location: tests/borrowck.rs:2025
#[test]
fn min_problem_case_3() {
FormalityTest::new(feature_gate_program(NLL_GATE, MIN_PROBLEM_CASE_3))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
&access.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {!lt_1, ?lt_2, ?lt_3}
&lifetime.upcast() = !lt_1
the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
{
Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
{
Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
Lt::Variable(Variable::ExistentialVar(_)) => true,
Lt::Variable(Variable::BoundVar(_)) =>
panic!("cannot outlive a bound var"), Lt::Erased => true,
}, Parameter::Const(_) => panic!("cannot outlive a constant"),
})`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `m`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
place_loaned_ref = m : &!lt_1 mut Map"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
MIN_PROBLEM_CASE_3,
))
.skip_execute()
.ok();
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
MIN_PROBLEM_CASE_3,
))
.skip_execute()
.ok();
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54args
for_allmod.rs:41for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
Source location: tests/borrowck.rs:2032
#[test]
fn min_problem_case_3() {
FormalityTest::new(feature_gate_program(NLL_GATE, MIN_PROBLEM_CASE_3))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
&access.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {!lt_1, ?lt_2, ?lt_3}
&lifetime.upcast() = !lt_1
the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
{
Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
{
Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
Lt::Variable(Variable::ExistentialVar(_)) => true,
Lt::Variable(Variable::BoundVar(_)) =>
panic!("cannot outlive a bound var"), Lt::Erased => true,
}, Parameter::Const(_) => panic!("cannot outlive a constant"),
})`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `m`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
place_loaned_ref = m : &!lt_1 mut Map"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
MIN_PROBLEM_CASE_3,
))
.skip_execute()
.ok();
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
MIN_PROBLEM_CASE_3,
))
.skip_execute()
.ok();
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54args
for_allmod.rs:41for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
Source location: tests/borrowck.rs:2220
fn min_problem_case_3<'a>(m: &'a mut Map) -> &'a mut Map {
exists<'r0, 'r1> {
let n: &'r0 mut Map = &mut 'r0 *m;
if true {
} else {
}
let o: &'r1 mut Map = &mut 'r1 *m;
return o;
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54args
for_allmod.rs:41for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
Source location: tests/borrowck.rs:2341
fn min_problem_case_4<'a>(list: &'a mut Map, list2: &'a mut Map) -> u32 {
exists<'r0> {
let num: &'r0 mut u32 = &mut 'r0 (*list).value;
list = &mut 'a *list2;
num;
return 0_u32;
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54args
for_allmod.rs:41for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
Source location: tests/borrowck.rs:2831
#[test]
fn if_false_borrowck() {
FormalityTest::new(feature_gate_program(NLL_GATE, IF_FALSE_BORROWCK))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
&access.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {!lt_1, ?lt_2, ?lt_3}
&lifetime.upcast() = !lt_1
the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
{
Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
{
Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
Lt::Variable(Variable::ExistentialVar(_)) => true,
Lt::Variable(Variable::BoundVar(_)) =>
panic!("cannot outlive a bound var"), Lt::Erased => true,
}, Parameter::Const(_) => panic!("cannot outlive a constant"),
})`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `m`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
place_loaned_ref = m : &!lt_1 mut Map"#]]);
FormalityTest::new(feature_gate_program(POLONIUS_ALPHA_GATE, IF_FALSE_BORROWCK))
.skip_execute()
.ok();
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
IF_FALSE_BORROWCK,
))
.skip_execute()
.ok();
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54args
for_allmod.rs:41for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:79args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:313args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:39args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:87args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:126args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
Source location: tests/borrowck.rs:2838
#[test]
fn if_false_borrowck() {
FormalityTest::new(feature_gate_program(NLL_GATE, IF_FALSE_BORROWCK))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
&access.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {!lt_1, ?lt_2, ?lt_3}
&lifetime.upcast() = !lt_1
the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
{
Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
{
Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
Lt::Variable(Variable::ExistentialVar(_)) => true,
Lt::Variable(Variable::BoundVar(_)) =>
panic!("cannot outlive a bound var"), Lt::Erased => true,
}, Parameter::Const(_) => panic!("cannot outlive a constant"),
})`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `m`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
place_loaned_ref = m : &!lt_1 mut Map"#]]);
FormalityTest::new(feature_gate_program(POLONIUS_ALPHA_GATE, IF_FALSE_BORROWCK))
.skip_execute()
.ok();
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
IF_FALSE_BORROWCK,
))
.skip_execute()
.ok();
}
Proof trees omitted for the remaining 53 tests.
Source location: tests/borrowck.rs:3081
fn foo() -> u32 {
exists<'r0, 'r1, 'r2, 'r3> {
let p: Point = Point { x: 0_u32, y: 0_u32 };
let b1: &'r0 mut u32 = &mut 'r1 p.x;
let b2: &'r2 mut u32 = &mut 'r3 p.y;
*b1 = 1_u32;
*b2 = 2_u32;
return 0_u32;
}
}
Source location: tests/borrowck.rs:3683
#[test]
fn issue_63908_remove_last_node_recursive() {
// [nll]: rustc passes.
FormalityTest::new(feature_gate_program(
NLL_GATE,
ISSUE_63908_REMOVE_LAST_NODE_RECURSIVE,
))
.skip_execute()
.ok();
// [polonius]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_63908_REMOVE_LAST_NODE_RECURSIVE,
))
.skip_execute()
.ok();
// [legacy]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_63908_REMOVE_LAST_NODE_RECURSIVE,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:3691
#[test]
fn issue_63908_remove_last_node_recursive() {
// [nll]: rustc passes.
FormalityTest::new(feature_gate_program(
NLL_GATE,
ISSUE_63908_REMOVE_LAST_NODE_RECURSIVE,
))
.skip_execute()
.ok();
// [polonius]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_63908_REMOVE_LAST_NODE_RECURSIVE,
))
.skip_execute()
.ok();
// [legacy]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_63908_REMOVE_LAST_NODE_RECURSIVE,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:3699
#[test]
fn issue_63908_remove_last_node_recursive() {
// [nll]: rustc passes.
FormalityTest::new(feature_gate_program(
NLL_GATE,
ISSUE_63908_REMOVE_LAST_NODE_RECURSIVE,
))
.skip_execute()
.ok();
// [polonius]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_63908_REMOVE_LAST_NODE_RECURSIVE,
))
.skip_execute()
.ok();
// [legacy]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_63908_REMOVE_LAST_NODE_RECURSIVE,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:3801
#[test]
fn issue_63908_remove_last_node_iterative() {
FormalityTest::new(feature_gate_program(
NLL_GATE,
ISSUE_63908_REMOVE_LAST_NODE_ITERATIVE,
))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
&access.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {?lt_2, ?lt_3}
&lifetime.upcast() = ?lt_2
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `cursor`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
place_loaned_ref = cursor : &?lt_2 mut List"#]]);
// [polonius]: rustc errors here (known-bug #63908), same as [nll].
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_63908_REMOVE_LAST_NODE_ITERATIVE,
))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
&access.place = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {?lt_2, ?lt_3}
&lifetime.upcast() = ?lt_2
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `cursor`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(cursor : &?lt_2 mut List) : <&?lt_2 mut List as Derefable>::Target
place_loaned_ref = cursor : &?lt_2 mut List"#]]);
// [legacy]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_63908_REMOVE_LAST_NODE_ITERATIVE,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:3849
#[test]
fn issue_57165_no_control_flow() {
// [nll]: rustc passes.
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_57165_NO_CONTROL_FLOW))
.skip_execute()
.ok();
// [polonius]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_57165_NO_CONTROL_FLOW,
))
.skip_execute()
.ok();
// [legacy]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_57165_NO_CONTROL_FLOW,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:3857
#[test]
fn issue_57165_no_control_flow() {
// [nll]: rustc passes.
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_57165_NO_CONTROL_FLOW))
.skip_execute()
.ok();
// [polonius]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_57165_NO_CONTROL_FLOW,
))
.skip_execute()
.ok();
// [legacy]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_57165_NO_CONTROL_FLOW,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:3865
#[test]
fn issue_57165_no_control_flow() {
// [nll]: rustc passes.
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_57165_NO_CONTROL_FLOW))
.skip_execute()
.ok();
// [polonius]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_57165_NO_CONTROL_FLOW,
))
.skip_execute()
.ok();
// [legacy]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_57165_NO_CONTROL_FLOW,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4011
#[test]
fn issue_57165_conditional() {
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_57165_CONDITIONAL))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "fixed-point" at (nll.rs) failed because
condition evaluated to false: `state0 == state1`
state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)})
state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)})
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
&access.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {?lt_1, ?lt_3, ?lt_4}
&lifetime.upcast() = ?lt_1
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `p`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
place_loaned_ref = p : &?lt_1 mut X
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
&access.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {?lt_1, ?lt_3, ?lt_4}
&lifetime.upcast() = ?lt_1
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `p`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
place_loaned_ref = p : &?lt_1 mut X"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_57165_CONDITIONAL,
))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "fixed-point" at (nll.rs) failed because
condition evaluated to false: `state0 == state1`
state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)})
state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)})
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
&access.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {?lt_1, ?lt_3, ?lt_4}
&lifetime.upcast() = ?lt_1
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `p`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
place_loaned_ref = p : &?lt_1 mut X
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
&access.place = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {?lt_1, ?lt_3, ?lt_4}
&lifetime.upcast() = ?lt_1
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `p`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target
place_loaned_ref = p : &?lt_1 mut X"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_57165_CONDITIONAL,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4066
#[test]
fn issue_57165_conditional_with_indirection() {
// [nll]: rustc passes
FormalityTest::new(feature_gate_program(
NLL_GATE,
ISSUE_57165_CONDITIONAL_WITH_INDIRECTION,
))
.skip_execute()
.ok();
// [polonius]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_57165_CONDITIONAL_WITH_INDIRECTION,
))
.skip_execute()
.ok();
// [legacy]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_57165_CONDITIONAL_WITH_INDIRECTION,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4074
#[test]
fn issue_57165_conditional_with_indirection() {
// [nll]: rustc passes
FormalityTest::new(feature_gate_program(
NLL_GATE,
ISSUE_57165_CONDITIONAL_WITH_INDIRECTION,
))
.skip_execute()
.ok();
// [polonius]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_57165_CONDITIONAL_WITH_INDIRECTION,
))
.skip_execute()
.ok();
// [legacy]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_57165_CONDITIONAL_WITH_INDIRECTION,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4082
#[test]
fn issue_57165_conditional_with_indirection() {
// [nll]: rustc passes
FormalityTest::new(feature_gate_program(
NLL_GATE,
ISSUE_57165_CONDITIONAL_WITH_INDIRECTION,
))
.skip_execute()
.ok();
// [polonius]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_57165_CONDITIONAL_WITH_INDIRECTION,
))
.skip_execute()
.ok();
// [legacy]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_57165_CONDITIONAL_WITH_INDIRECTION,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4137
#[test]
fn issue_46859_to_refs() {
// [nll]: rustc passes
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_46859_TO_REFS))
.skip_execute()
.ok();
// [polonius]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_46859_TO_REFS,
))
.skip_execute()
.ok();
// [legacy]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_46859_TO_REFS,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4145
#[test]
fn issue_46859_to_refs() {
// [nll]: rustc passes
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_46859_TO_REFS))
.skip_execute()
.ok();
// [polonius]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_46859_TO_REFS,
))
.skip_execute()
.ok();
// [legacy]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_46859_TO_REFS,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4153
#[test]
fn issue_46859_to_refs() {
// [nll]: rustc passes
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_46859_TO_REFS))
.skip_execute()
.ok();
// [polonius]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_46859_TO_REFS,
))
.skip_execute()
.ok();
// [legacy]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_46859_TO_REFS,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4191
#[test]
fn issue_46859_to_refs2() {
// [nll]: rustc passes.
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_46859_TO_REFS2))
.skip_execute()
.ok();
// [polonius]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_46859_TO_REFS2,
))
.skip_execute()
.ok();
// [legacy]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_46859_TO_REFS2,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4199
#[test]
fn issue_46859_to_refs2() {
// [nll]: rustc passes.
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_46859_TO_REFS2))
.skip_execute()
.ok();
// [polonius]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_46859_TO_REFS2,
))
.skip_execute()
.ok();
// [legacy]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_46859_TO_REFS2,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4207
#[test]
fn issue_46859_to_refs2() {
// [nll]: rustc passes.
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_46859_TO_REFS2))
.skip_execute()
.ok();
// [polonius]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_46859_TO_REFS2,
))
.skip_execute()
.ok();
// [legacy]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_46859_TO_REFS2,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4256
#[test]
fn issue_46859_to_refs3() {
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_46859_TO_REFS3))
.skip_execute()
.ok();
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_46859_TO_REFS3,
))
.skip_execute()
.ok();
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_46859_TO_REFS3,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4263
#[test]
fn issue_46859_to_refs3() {
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_46859_TO_REFS3))
.skip_execute()
.ok();
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_46859_TO_REFS3,
))
.skip_execute()
.ok();
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_46859_TO_REFS3,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4270
#[test]
fn issue_46859_to_refs3() {
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_46859_TO_REFS3))
.skip_execute()
.ok();
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_46859_TO_REFS3,
))
.skip_execute()
.ok();
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_46859_TO_REFS3,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4394
#[test]
fn issue_46859_decoder_next() {
// [nll]: rustc errors
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_46859_DECODER_NEXT))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "fixed-point" at (nll.rs) failed because
condition evaluated to false: `state0 == state1`
state0 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)})
state1 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {loan(?lt_2, *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32, mut)}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)})
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
&access.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {!lt_1, ?lt_2, ?lt_3}
&lifetime.upcast() = !lt_1
the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
{
Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
{
Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
Lt::Variable(Variable::ExistentialVar(_)) => true,
Lt::Variable(Variable::BoundVar(_)) =>
panic!("cannot outlive a bound var"), Lt::Erased => true,
}, Parameter::Const(_) => panic!("cannot outlive a constant"),
})`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct]`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `d`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
place_loaned_ref = d : &!lt_1 mut Decoder
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
&access.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {!lt_1, ?lt_2, ?lt_3}
&lifetime.upcast() = !lt_1
the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
{
Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
{
Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
Lt::Variable(Variable::ExistentialVar(_)) => true,
Lt::Variable(Variable::BoundVar(_)) =>
panic!("cannot outlive a bound var"), Lt::Erased => true,
}, Parameter::Const(_) => panic!("cannot outlive a constant"),
})`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct]`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `d`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
place_loaned_ref = d : &!lt_1 mut Decoder"#]]);
// [polonius]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_46859_DECODER_NEXT,
))
.skip_execute()
.ok();
// [legacy]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_46859_DECODER_NEXT,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4402
#[test]
fn issue_46859_decoder_next() {
// [nll]: rustc errors
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_46859_DECODER_NEXT))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "fixed-point" at (nll.rs) failed because
condition evaluated to false: `state0 == state1`
state0 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)})
state1 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {loan(?lt_2, *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32, mut)}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)})
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
&access.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {!lt_1, ?lt_2, ?lt_3}
&lifetime.upcast() = !lt_1
the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
{
Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
{
Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
Lt::Variable(Variable::ExistentialVar(_)) => true,
Lt::Variable(Variable::BoundVar(_)) =>
panic!("cannot outlive a bound var"), Lt::Erased => true,
}, Parameter::Const(_) => panic!("cannot outlive a constant"),
})`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct]`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `d`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
place_loaned_ref = d : &!lt_1 mut Decoder
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
&access.place = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {!lt_1, ?lt_2, ?lt_3}
&lifetime.upcast() = !lt_1
the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
{
Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
{
Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
Lt::Variable(Variable::ExistentialVar(_)) => true,
Lt::Variable(Variable::BoundVar(_)) =>
panic!("cannot outlive a bound var"), Lt::Erased => true,
}, Parameter::Const(_) => panic!("cannot outlive a constant"),
})`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct]`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `d`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32
place_loaned_ref = d : &!lt_1 mut Decoder"#]]);
// [polonius]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_46859_DECODER_NEXT,
))
.skip_execute()
.ok();
// [legacy]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_46859_DECODER_NEXT,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4536
#[test]
fn issue_92985_filtering_lending_iterator() {
// [nll]: rustc errors
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_92985_FILTER_NEXT))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "fixed-point" at (nll.rs) failed because
condition evaluated to false: `state0 == state1`
state0 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)})
state1 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut), loan(?lt_3, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . predicate[Filter , struct] : u32, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut)}, {}))}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)})
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
&access.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {!lt_1, ?lt_2, ?lt_3, ?lt_4}
&lifetime.upcast() = !lt_1
the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
{
Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
{
Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
Lt::Variable(Variable::ExistentialVar(_)) => true,
Lt::Variable(Variable::BoundVar(_)) =>
panic!("cannot outlive a bound var"), Lt::Erased => true,
}, Parameter::Const(_) => panic!("cannot outlive a constant"),
})`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct]`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `f`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
place_loaned_ref = f : &!lt_1 mut Filter
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
&access.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {!lt_1, ?lt_2, ?lt_3, ?lt_4}
&lifetime.upcast() = !lt_1
the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
{
Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
{
Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
Lt::Variable(Variable::ExistentialVar(_)) => true,
Lt::Variable(Variable::BoundVar(_)) =>
panic!("cannot outlive a bound var"), Lt::Erased => true,
}, Parameter::Const(_) => panic!("cannot outlive a constant"),
})`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct]`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `f`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
place_loaned_ref = f : &!lt_1 mut Filter"#]]);
// [polonius]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_92985_FILTER_NEXT,
))
.skip_execute()
.ok();
// [legacy]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_92985_FILTER_NEXT,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4544
#[test]
fn issue_92985_filtering_lending_iterator() {
// [nll]: rustc errors
FormalityTest::new(feature_gate_program(NLL_GATE, ISSUE_92985_FILTER_NEXT))
.skip_execute()
.err(expect_test::expect![[r#"
the rule "fixed-point" at (nll.rs) failed because
condition evaluated to false: `state0 == state1`
state0 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)})
state1 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut), loan(?lt_3, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . predicate[Filter , struct] : u32, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut)}, {}))}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)})
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
&access.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {!lt_1, ?lt_2, ?lt_3, ?lt_4}
&lifetime.upcast() = !lt_1
the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
{
Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
{
Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
Lt::Variable(Variable::ExistentialVar(_)) => true,
Lt::Variable(Variable::BoundVar(_)) =>
panic!("cannot outlive a bound var"), Lt::Erased => true,
}, Parameter::Const(_) => panic!("cannot outlive a constant"),
})`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct]`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `f`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
place_loaned_ref = f : &!lt_1 mut Filter
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
&access.place = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {!lt_1, ?lt_2, ?lt_3, ?lt_4}
&lifetime.upcast() = !lt_1
the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
{
Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
{
Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
Lt::Variable(Variable::ExistentialVar(_)) => true,
Lt::Variable(Variable::BoundVar(_)) =>
panic!("cannot outlive a bound var"), Lt::Erased => true,
}, Parameter::Const(_) => panic!("cannot outlive a constant"),
})`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `*(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct]`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `f`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32
place_loaned_ref = f : &!lt_1 mut Filter"#]]);
// [polonius]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
ISSUE_92985_FILTER_NEXT,
))
.skip_execute()
.ok();
// [legacy]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
ISSUE_92985_FILTER_NEXT,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4618
#[test]
fn flow_sensitive_invariance_use_it() {
// [nll]: rustc errors
FormalityTest::new(feature_gate_program(
NLL_GATE,
FLOW_SENSITIVE_INVARIANCE_USE_IT,
))
.skip_execute()
.err(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
// [polonius]: rustc errors
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
FLOW_SENSITIVE_INVARIANCE_USE_IT,
))
.skip_execute()
.err(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:8:1: no applicable rules for prove_via { goal: !lt_1 : !lt_2, via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_1, b: !lt_2, assumptions: {@ wf(?lt_0)}, env: Env { variables: [!lt_1, !lt_2, ?lt_0], bias: Soundness, pending: [], allow_pending_outlives: false } }"#]]);
// [legacy]: rustc passes
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
FLOW_SENSITIVE_INVARIANCE_USE_IT,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4711
#[test]
fn flow_sensitive_invariance_same_region() {
// [nll]: rustc passes.
FormalityTest::new(feature_gate_program(
NLL_GATE,
FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
))
.skip_execute()
.ok();
// [polonius]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
))
.skip_execute()
.ok();
// [legacy]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4719
#[test]
fn flow_sensitive_invariance_same_region() {
// [nll]: rustc passes.
FormalityTest::new(feature_gate_program(
NLL_GATE,
FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
))
.skip_execute()
.ok();
// [polonius]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
))
.skip_execute()
.ok();
// [legacy]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:4727
#[test]
fn flow_sensitive_invariance_same_region() {
// [nll]: rustc passes.
FormalityTest::new(feature_gate_program(
NLL_GATE,
FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
))
.skip_execute()
.ok();
// [polonius]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
))
.skip_execute()
.ok();
// [legacy]: rustc passes.
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
FLOW_SENSITIVE_INVARIANCE_SAME_REGION,
))
.skip_execute()
.ok();
}
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:264
fn main() -> () {
let w: Wrapper<i32> = Wrapper::<i32> { val: 42_i32 };
println!(w.val);
}
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:98
#[test]
fn covered_VecT() {
FormalityTest::new(crates![crate core {
trait CoreTrait<T> {}
struct Vec<T> {}
},
crate foo {
struct FooStruct {}
impl<T> CoreTrait<FooStruct> for Vec<T> {}
}])
.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:147
#[test]
fn neg_CoreTrait_for_CoreStruct_implies_no_overlap() {
FormalityTest::new(crates![crate core {
trait CoreTrait {}
struct CoreStruct {}
impl !CoreTrait for CoreStruct {}
},
crate foo {
trait FooTrait {}
impl<T> FooTrait for T where T: CoreTrait {}
impl FooTrait for CoreStruct {}
}])
.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/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/drop.rs:94
#[test]
fn drop_impl_enum() {
FormalityTest::new(crates![
crate Foo {
enum MyEnum {
Variant{},
}
impl Drop for MyEnum {}
}
])
.skip_execute()
.ok()
}
Source location: tests/drop.rs:111
#[test]
fn drop_impl_cross_crate_local() {
FormalityTest::new(crates![
crate a {
struct MyStruct {
value: u32,
}
impl Drop for MyStruct {}
},
crate b {}
])
.skip_execute()
.ok()
}
Source location: tests/field_projections.rs:17
fn test(ptr: Ptr) -> () {
let x: () = *ptr;
}
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:857
fn foo<'a>(v1: &'a Pair) -> u32 {
exists<'r0> {
let v2: u32 = (*v1).value;
return v2;
}
}
Source location: tests/references.rs:36
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()
}