Judgment borrow_check_place_expr at crates/formality-rust/src/check/borrow_check/nll.rs:563
Signature:
borrow_check_place_expr(env: TypeckEnv, assumptions: Wcs, state: FlowState, place: PlaceExpr,) => (TypedPlaceExpr, FlowState)
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 |
|---|---|---|
| 574 | 2 | (let ty = state.local_variable(&local_id)?) |
| ──────── ("local") | ||
| 576 | 58 | (borrow_check_place_expr(_env, _assumptions, state, PlaceExpr::Var(local_id)) => ( TypedPlaceExpr::new(ty, TypedPlaceExpressionData::local(local_id)), state, )) |
struct field| Line | Coverage | Source |
|---|---|---|
| 583 | ✗ | (borrow_check_place_expr(env, assumptions, state, prefix) => (prefix_typed, state)) |
| 584 | 1 | (prove_ty_is_rigid(env, assumptions, state, &prefix_typed.ty) => (RigidTy { name: RigidName::AdtId(adt_id), parameters }, state)) |
| 585 | ✗ | (let Struct { id: _, binder } = env.crates().struct_named(&adt_id)?) |
| 586 | ✗ | (let StructBoundData { where_clauses, fields } = binder.instantiate_with(¶meters)?) |
| 587 | ✗ | (prove_where_clauses(env, assumptions, state, where_clauses) => state) |
| 588 | ✗ | (field in fields) |
| 589 | 1 | (if field.name == *field_name) |
| ──────── ("struct field") | ||
| 591 | 7 | (borrow_check_place_expr(env, assumptions, state, PlaceExpr::Field { prefix, field_name }) => ( TypedPlaceExpr::new(&field.ty, TypedPlaceExpressionData::field(prefix_typed, field_name)), state, )) |
tuple field| Line | Coverage | Source |
|---|---|---|
| 598 | ✗ | (borrow_check_place_expr(env, assumptions, state, prefix) => (prefix_typed, state)) |
| 599 | ✗ | (prove_ty_is_rigid(env, assumptions, state, &prefix_typed.ty) => (RigidTy { name: RigidName::Tuple(arity), parameters }, state)) |
| 600 | ✗ | (if field_index < arity) |
| 601 | ✗ | (if let Parameter::Ty(field_ty) = ¶meters[*field_index]) |
| ──────── ("tuple field") | ||
| 603 | ✗ | (borrow_check_place_expr(env, assumptions, state, PlaceExpr::Field { prefix, field_name: FieldName::Index(field_index) }) => ( TypedPlaceExpr::new(field_ty, TypedPlaceExpressionData::field(prefix_typed, field_index)), state, )) |
parens| Line | Coverage | Source |
|---|---|---|
| 610 | ✗ | (borrow_check_place_expr(env, assumptions, state, place) => (place_typed, state)) |
| ──────── ("parens") | ||
| 612 | 2 | (borrow_check_place_expr(env, assumptions, state, PlaceExpr::Parens(place)) => (place_typed, state)) |
deref-ref| Line | Coverage | Source |
|---|---|---|
| 616 | ✗ | (borrow_check_place_expr(env, assumptions, state, prefix) => (prefix_typed, state)) |
| 617 | ✗ | (prove_is_implemented(env, assumptions, state, TraitId::new("Derefable").with_self(&prefix_typed.ty)) => state) |
| 618 | N/A | (let referent_ty = AliasTy::associated_ty( TraitId::new("Derefable"), AssociatedItemId::new("Target"), 0, vec![&prefix_typed.ty], )) |
| ──────── ("deref-ref") | ||
| 625 | 18 | (borrow_check_place_expr(env, assumptions, state, PlaceExpr::Deref { prefix }) => ( TypedPlaceExpr::new(referent_ty, TypedPlaceExpressionData::deref(prefix_typed)), state, )) |