Judgment access_permitted_by_loans
judgment_fn! {
/// Prove that none of the borrows in `borrowed` does not affect `place`.
fn access_permitted_by_loans(
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:885
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_by_loans| Line | Coverage | Source |
|---|---|---|
| 897 | ✗ | (for_all(loan in &state.current.loans_live) with(state) (access_permitted_by_loan(env, assumptions, state, loan, access, places_live_after_access) => state)) |
| ──────── ("access_permitted_by_loans") | ||
| 900 | 106 | (access_permitted_by_loans(env, assumptions, state, access, places_live_after_access) => state) |