Judgment loan_not_required_by_live_place_prefix
judgment_fn! {
/// For some `place_live` where
///
/// let x = &'lt_loan place_borrowed;
/// ...
/// access(place_accessed); // conflicts with the borrow
/// ...
/// access(place_live) // <-- an access like this occurs later
///
/// ...show that `place_live` does not require data derived from `x`.
fn loan_not_required_by_live_place_prefix(
env: TypeckEnv,
assumptions: Predicates,
outlives: Set<PendingOutlives>,
loan: Loan,
live_place: TypedPlaceExpr,
) => () {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/borrow_check/nll.rs:1362
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.
no prefix| Line | Coverage | Source |
|---|---|---|
| 1382 | ✗ | (if let None = live_place.prefix()) |
| ──────── ("no prefix") | ||
| 1384 | 12 | (loan_not_required_by_live_place_prefix(_env, _assumptions, _outlives, _loan, live_place) => ()) |
prefix| Line | Coverage | Source |
|---|---|---|
| 1388 | ✗ | (if let Some(prefix) = live_place.prefix()) |
| 1389 | ✗ | (loan_not_required_by_live_place(env, assumptions, outlives, loan, prefix) => ()) |
| ──────── ("prefix") | ||
| 1391 | 3 | (loan_not_required_by_live_place_prefix(env, assumptions, outlives, loan, live_place) => ()) |