Judgment access_permitted_by_loan
judgment_fn! {
/// Prove that the borrow `borrow` does not affect `place`.
fn access_permitted_by_loan(
env: TypeckEnv,
assumptions: Predicates,
state: FlowState,
loan: Loan,
access: Access,
places_live_after_access: LivePlaces,
) => FlowState {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/borrow_check/nll.rs:905
The 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 |
|---|---|---|
| 920 | 29 | (if place_disjoint_from_place(&loan.place, &access.place)) |
| ──────── ("borrow of disjoint places") | ||
| 922 | 41 | (access_permitted_by_loan(_env, _assumptions, state, loan, access, _places_live_after_access) => state) |
write-indirect| Line | Coverage | Source |
|---|---|---|
| 946 | ✗ | (place_loaned in place_loaned.all_prefixes()) |
| 947 | 24 | (if let TypedPlaceExpressionData::Deref(place_loaned_ref) = place_loaned.data()) |
| 948 | ✗ | (prove_ty_is_ref(env, assumptions, state, &place_loaned_ref.ty) => state) |
| 949 | 8 | (if place_accessed.is_prefix_of(place_loaned_ref)) |
| ──────── ("write-indirect") | ||
| 951 | 10 | (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 |
|---|---|---|
| 965 | ✗ | (if !place_disjoint_from_place(&loan.place, &access.place)) |
| 966 | N/A | (let places_live = places_live_for_loan(env, access, places_live_after_access)) |
| 967 | 29 | (loan_not_required_by_live_places(env, assumptions, state, loan, places_live) => state) |
| 968 | ✗ | (loan_cannot_outlive_universal_regions(env, assumptions, &state.current.outlives, &loan) => ()) |
| ──────── ("loan is dead") | ||
| 970 | 18 | (access_permitted_by_loan(env, assumptions, state, loan, access, places_live_after_access) => state) |