Judgment access_permitted_by_loan at crates/formality-rust/src/check/borrow_check/nll.rs:733
Signature:
access_permitted_by_loan(env: TypeckEnv, assumptions: Wcs, state: FlowState, loan: Loan, access: Access, places_live_after_access: LivePlaces,) => FlowStateThe number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.
borrow of disjoint places| Line | Coverage | Source |
|---|---|---|
| 748 | 15 | (if place_disjoint_from_place(&loan.place, &access.place)) |
| ──────── ("borrow of disjoint places") | ||
| 750 | 17 | (access_permitted_by_loan(_env, _assumptions, state, loan, access, _places_live_after_access) => state) |
write-indirect| Line | Coverage | Source |
|---|---|---|
| 774 | ✗ | (place_loaned in place_loaned.all_prefixes()) |
| 775 | 13 | (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") | ||
| 779 | 1 | (access_permitted_by_loan( env, assumptions, state, Loan { lt: _, place: place_loaned, kind: _ }, Access { kind: AccessKind::Write, place: place_accessed }, _live_places, ) => state) |
loan is dead| Line | Coverage | Source |
|---|---|---|
| 793 | ✗ | (if !place_disjoint_from_place(&loan.place, &access.place)) |
| 794 | 15 | (loan_not_required_by_live_places(env, assumptions, state, loan, places_live_after_access) => state) |
| 795 | ✗ | (loan_cannot_outlive_universal_regions(env, assumptions, &state.current.outlives, &loan) => ()) |
| ──────── ("loan is dead") | ||
| 797 | 9 | (access_permitted_by_loan(env, assumptions, state, loan, access, places_live_after_access) => state) |