Judgment access_permitted_by_loan at crates/formality-rust/src/check/borrow_check/nll.rs:840
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 |
|---|---|---|
| 855 | 25 | (if place_disjoint_from_place(&loan.place, &access.place)) |
| ──────── ("borrow of disjoint places") | ||
| 857 | 45 | (access_permitted_by_loan(_env, _assumptions, state, loan, access, _places_live_after_access) => state) |
write-indirect| Line | Coverage | Source |
|---|---|---|
| 881 | ✗ | (place_loaned in place_loaned.all_prefixes()) |
| 882 | 23 | (if let TypedPlaceExpressionData::Deref(place_loaned_ref) = place_loaned.data()) |
| 883 | ✗ | (prove_ty_is_ref(env, assumptions, state, &place_loaned_ref.ty) => state) |
| 884 | 9 | (if place_accessed.is_prefix_of(place_loaned_ref)) |
| ──────── ("write-indirect") | ||
| 886 | 20 | (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 |
|---|---|---|
| 900 | ✗ | (if !place_disjoint_from_place(&loan.place, &access.place)) |
| 901 | N/A | (let places_live = places_live_for_loan(env, access, places_live_after_access)) |
| 902 | 25 | (loan_not_required_by_live_places(env, assumptions, state, loan, places_live) => state) |
| 903 | ✗ | (loan_cannot_outlive_universal_regions(env, assumptions, &state.current.outlives, &loan) => ()) |
| ──────── ("loan is dead") | ||
| 905 | 24 | (access_permitted_by_loan(env, assumptions, state, loan, access, places_live_after_access) => state) |