Judgment loan_not_required_by_live_places
judgment_fn! {
/// Prove that the `loan` is not required to be live by
/// an access to any of the places in `places_live_after_access`.
///
/// For each `place_live \in places_live_after_acecess`...
///
/// let x = &'lt_loan place_borrowed;
/// ...
/// access(place_accessed); // conflicts with the borrow
/// ...
/// access(place_live)
///
/// ...show that `place_live` does not require data derived from `x`.
fn loan_not_required_by_live_places(
env: TypeckEnv,
assumptions: Predicates,
state: FlowState,
loan: Loan,
places_live_after_access: LivePlaces,
) => FlowState {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/borrow_check/nll.rs:1296
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.
loan_not_required_by_live_places| Line | Coverage | Source |
|---|---|---|
| 1319 | ✗ | (for_all(live_place in places_live_after_access) with(state) (borrow_check_place_expr(env, assumptions, state, live_place) => (live_place_typed, state)) (loan_not_required_by_live_place(env, assumptions, &state.current.outlives, loan, live_place_typed) => ())) |
| ──────── ("loan_not_required_by_live_places") | ||
| 1323 | 18 | (loan_not_required_by_live_places(env, assumptions, state, loan, places_live_after_access) => state) |