Positive coverage: prove_sub / normalize-l
normalize-l| Line | Coverage | Source |
|---|---|---|
| 27 | 5 | (prove_normalize(decls, env, assumptions, x) => Constrained(y, c)) |
| 28 | ✗ | (prove_after(decls, c, assumptions, Relation::sub(y, z)) => c) |
| ──────── ("normalize-l") | ||
| 30 | 36 | (prove_sub(decls, env, assumptions, x, z) => c) |
36 tests exercised this rule:
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:2105
fn foo() -> i32 {
exists<'r0, 'r1> {
let result: i32;
{
let v1: i32 = 22_i32;
let v2: &'r0 i32 = &'r1 v1;
result = *v2;
}
return result;
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs: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:2474
fn foo () -> u32 {
exists<'l_p, 'l_q, 'loan_0, 'loan_1, 'loan_2, 'loan_3> {
let a: u32 = 0_u32;
let b: u32 = 0_u32;
// In Rustc, the 1-tuple is needed for some reason
// Niko does not 100% understand, else rustc is able to
// see that this program is safe.
let q: &'l_q mut u32 = &mut 'loan_0 a;
let p: &'l_p mut u32 = &mut 'loan_1 a;
if true {
p = &mut 'loan_1 a;
q = &mut 'loan_2 b;
} else {
p = &mut 'loan_3 b;
}
*q = 1_u32;
return *p;
}
}
Proof 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:2664
fn foo() -> u32 {
exists<'r0, 'r1> {
'a: loop {
let x: i32 = 0_i32;
let r: &'r0 i32 = &'r1 x;
let _y: i32 = *r;
continue 'a;
}
}
}
Proof tree
check_all_crates (check all prefixes)mod.rs: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 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:2933
fn bar() -> u32 {
exists<'r1> {
let v: u32 = 7_u32;
let r: u32 = foo::<'r1>(&'r1 v);
return r;
}
}
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:3027
fn bar() -> u32 {
exists<'r0, 'r1> {
let v: u32 = 1_u32;
let p: &'r0 u32 = &'r1 v;
foo(0_u32);
return *p;
}
}
Proof trees omitted for the remaining 26 tests.
Source location: tests/borrowck.rs:3200
fn reborrow<'a>(a: &'a mut u8) -> &'a mut u8 {
exists<'r0, 'r1, 'r2, 'r3> {
if true {
let b: &'r1 mut u8 = &mut 'r0 *a;
return b;
} else { }
let c: &'r3 mut u8 = &mut 'r2 *a;
return c;
}
}
Source location: tests/borrowck.rs:3266
#[test]
fn outlive_before_return_does_not_affect_merged_paths() {
FormalityTest::new(feature_gate_program(
NLL_GATE,
OUTLIVE_BEFORE_RETURN_DOES_NOT_AFFECT_MERGED_PATHS,
))
.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 = *(a : &!lt_1 mut u8) : <&!lt_1 mut u8 as Derefable>::Target
&access.place = *(a : &!lt_1 mut u8) : <&!lt_1 mut u8 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, ?lt_4, ?lt_5}
&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 `a`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(a : &!lt_1 mut u8) : <&!lt_1 mut u8 as Derefable>::Target
place_loaned_ref = a : &!lt_1 mut u8"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
OUTLIVE_BEFORE_RETURN_DOES_NOT_AFFECT_MERGED_PATHS,
))
.skip_execute()
.ok();
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
OUTLIVE_BEFORE_RETURN_DOES_NOT_AFFECT_MERGED_PATHS,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:3273
#[test]
fn outlive_before_return_does_not_affect_merged_paths() {
FormalityTest::new(feature_gate_program(
NLL_GATE,
OUTLIVE_BEFORE_RETURN_DOES_NOT_AFFECT_MERGED_PATHS,
))
.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 = *(a : &!lt_1 mut u8) : <&!lt_1 mut u8 as Derefable>::Target
&access.place = *(a : &!lt_1 mut u8) : <&!lt_1 mut u8 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, ?lt_4, ?lt_5}
&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 `a`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(a : &!lt_1 mut u8) : <&!lt_1 mut u8 as Derefable>::Target
place_loaned_ref = a : &!lt_1 mut u8"#]]);
FormalityTest::new(feature_gate_program(
POLONIUS_ALPHA_GATE,
OUTLIVE_BEFORE_RETURN_DOES_NOT_AFFECT_MERGED_PATHS,
))
.skip_execute()
.ok();
FormalityTest::new(feature_gate_program(
POLONIUS_UNLOCKED_GATE,
OUTLIVE_BEFORE_RETURN_DOES_NOT_AFFECT_MERGED_PATHS,
))
.skip_execute()
.ok();
}
Source location: tests/borrowck.rs:3290
fn reborrow<'a>(a: &'a mut u8) -> &'a mut u8 {
exists<'r0, 'r1, 'r2, 'r3> {
let b: &'r1 mut u8 = &mut 'r0 *a;
return b;
let c: &'r3 mut u8 = &mut 'r2 *a;
return c;
}
}
Source location: tests/borrowck.rs:3310
fn reborrow<'a>(a: &'a mut u8) -> &'a mut u8 {
exists<'r0, 'r1, 'r2, 'r3> {
if true {
let b: &'r1 mut u8 = &mut 'r0 *a;
return b;
} else {
let c: &'r3 mut u8 = &mut 'r2 *a;
return c;
}
}
}
Source location: tests/borrowck.rs:3540
fn foo<'a, 'b>(p: &'a mut u32) -> u32 where 'a: 'b {
let q: &'b mut u32 = &mut 'b *p;
q;
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: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: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/field_projections.rs:17
fn test(ptr: Ptr) -> () {
let x: () = *ptr;
}
Source location: tests/mir_typeck.rs:710
fn foo () -> u32 {
exists<'a> {
let v0: u32 = 0_u32;
let v1: &'a u32 = &'a v0;
let v2: u32 = *v1;
return v2;
}
}
Source location: tests/mir_typeck.rs:729
fn foo<'a, T>(v1: &'a T) -> T
where
T: Copy,
T: 'a,
{
exists<'r0> {
let v2: T = *v1;
return v2;
}
}