Judgment drop_places
judgment_fn! {
/// Check that dropping the given locals (in the order provided) is permitted.
/// Locals should be provided in reverse declaration order (LIFO drop order).
fn drop_places(
env: TypeckEnv,
assumptions: Predicates,
state: FlowState,
places: Vec<TypedPlaceExpr>,
places_live_after_drop: LivePlaces,
) => FlowState {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/borrow_check/nll.rs:840
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.
drop_places| Line | Coverage | Source |
|---|---|---|
| 853 | ✗ | (for_all(place in places) with(state) (access_permitted_by_loans(env, assumptions, state, Access::new(AccessKind::Write, place), places_live_after_drop) => state) (let state = kill_loans(place, &state))) |
| ──────── ("drop_places") | ||
| 857 | 175 | (drop_places(env, assumptions, state, places, places_live_after_drop) => state) |