Judgment access_permitted
judgment_fn! {
/// Check that the given access is permitted.
fn access_permitted(
env: TypeckEnv,
assumptions: Predicates,
state: FlowState,
access: Access,
places_live_after_access: LivePlaces,
) => FlowState {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/borrow_check/nll.rs:862
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.
access_permitted| Line | Coverage | Source |
|---|---|---|
| 874 | 15 | (if match access.kind { AccessKind::Write => check_place_writable(&state, &access.place.to_place_expression()), AccessKind::Read | AccessKind::Move => check_place_initialized(&state, &access.place.to_place_expression()), }) |
| 878 | 24 | (access_permitted_by_loans(env, assumptions, state, access, places_live_after_access) => state) |
| ──────── ("access_permitted") | ||
| 880 | 103 | (access_permitted(env, assumptions, state, access, places_live_after_access) => state) |