Judgment prove_place_is_movable
judgment_fn! {
/// Prove that a place can be moved from.
///
/// A place is movable if it is not behind a reference. When a `Deref` is
/// encountered, the deref'd type must be an "owned deref" (e.g., `Box`).
/// Since we don't model owned deref types yet, all derefs through
/// references (`&T` / `&mut T`) will cause this judgment to fail.
fn prove_place_is_movable(
env: TypeckEnv,
assumptions: Predicates,
state: FlowState,
place: TypedPlaceExpr,
) => FlowState {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/borrow_check/nll.rs:1040
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.
local| Line | Coverage | Source |
|---|---|---|
| ──────── ("local") | ||
| 1057 | 89 | (prove_place_is_movable( _env, _assumptions, state, TypedPlaceExpressionData::Local(_), ) => state) |
field| Line | Coverage | Source |
|---|---|---|
| 1066 | 1 | (if let None = env.program.find_drop_impl(adt_id)) |
| 1067 | ✗ | (prove_place_is_movable(env, assumptions, state, prefix) => state) |
| ──────── ("field") | ||
| 1069 | 7 | (prove_place_is_movable( env, assumptions, state, TypedPlaceExpressionData::Field(prefix, _, adt_id, _), ) => state) |
copy| Line | Coverage | Source |
|---|---|---|
| 1078 | 3 | (prove_ty_is_copy(env, assumptions, state, &place.ty) => state) |
| ──────── ("copy") | ||
| 1080 | 17 | (prove_place_is_movable(env, assumptions, state, place) => state) |