Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Positive coverage: access_permitted_by_loan / write-indirect

write-indirect
LineCoverageSource
774✗(place_loaned in place_loaned.all_prefixes())
77513(if let TypedPlaceExpressionData::Deref(place_loaned_ref) = place_loaned.data())
776✗(prove_ty_is_ref(env, assumptions, state, &place_loaned_ref.ty) => state)
777✗(if place_accessed.is_prefix_of(place_loaned_ref))
──────── ("write-indirect")
7791(access_permitted_by_loan(
env,
assumptions,
state,
Loan { lt: _, place: place_loaned, kind: _ },
Access { kind: AccessKind::Write, place: place_accessed },
_live_places,
) => state)

1 test exercised this rule:

Source location: tests/borrowck.rs:2277

fn min_problem_case_4<'a>(list: &mut 'a Map, list2: &mut 'a Map) -> u32 {
    exists<'r0> {
        let num: &mut 'r0 u32 = &mut 'r0 (*list).value;
        list = &mut 'a *list2;
        num;
        return 0 _ u32;
    }
}
Proof tree
… (200 of 1262 nodes shown)