Judgment borrow_check_expr at crates/formality-rust/src/check/borrow_check/nll.rs:340
Signature:
borrow_check_expr(env: TypeckEnv, assumptions: Wcs, state: FlowState, expr: Expr, places_live_on_exit: LivePlaces,) => (Ty, 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.
assign| Line | Coverage | Source |
|---|---|---|
| 353 | ✗ | (borrow_check_expr( env, assumptions, state, expr, Assignment(place).live_before(env, &state, places_live_on_exit), ) => (value_ty, state)) |
| 362 | 2 | (borrow_check_place_expr( env, assumptions, state, place, ) => (place, state)) |
| 370 | 1 | (prove_assignable(env, assumptions, state, value_ty, &place.ty) => state) |
| 372 | 8 | (access_permitted( env, assumptions, state, Access::new(AccessKind::Write, place), places_live_on_exit, ) => state) |
| 380 | N/A | (let state = kill_loans(place, state)) |
| 381 | N/A | (let state = state.with_initialized(&place.to_place_expression())) |
| ──────── ("assign") | ||
| 383 | 13 | (borrow_check_expr(env, assumptions, state, Expr::Assign { place, expr }, places_live_on_exit) => (Ty::unit(), state)) |
call| Line | Coverage | Source |
|---|---|---|
| 388 | 3 | (borrow_check_expr( env, assumptions, state, callee, args.live_before(env, &state, places_live), ) => (callee_ty, state)) |
| 397 | ✗ | (prove_ty_is_rigid(env, assumptions, state, callee_ty) => (RigidTy { name: RigidName::FnDef(fn_id), parameters }, state)) |
| 400 | ✗ | (let Fn { id: _, safety, binder } = env.crates().fn_named(fn_id)?) |
| 402 | ✗ | (ProvenSet::singleton((safety, ProofTree::leaf("safety"))) => Safety::Safe) |
| 403 | ✗ | (let FnBoundData { input_args, output_ty, where_clauses, body: _ } = binder.instantiate_with(parameters)?) |
| 407 | N/A | (let input_tys: Vec<Ty> = input_args.iter().map(|a| a.ty.clone()).collect()) |
| 408 | 1 | (if input_tys.len() == args.len()) |
| 410 | ✗ | (for_all(i in 0..args.len()) with(state) (borrow_check_expr_has_ty(env, assumptions, state, &args[i], &input_tys[i], places_live) => state)) |
| 413 | ✗ | (prove_where_clauses(env, assumptions, state, where_clauses) => state) |
| ──────── ("call") | ||
| 415 | 14 | (borrow_check_expr(env, assumptions, state, Expr::Call { callee, args }, places_live) => (output_ty, state)) |
literal| Line | Coverage | Source |
|---|---|---|
| ──────── ("literal") | ||
| 420 | 48 | (borrow_check_expr(_env, _assumptions, state, Expr::Literal { value: _, ty }, _places_live_on_exit) => (ty, state)) |
true| Line | Coverage | Source |
|---|---|---|
| ──────── ("true") | ||
| 425 | 13 | (borrow_check_expr(_env, _assumptions, state, Expr::True, _places_live_on_exit) => (ScalarId::Bool, state)) |
false| Line | Coverage | Source |
|---|---|---|
| ──────── ("false") | ||
| 430 | 6 | (borrow_check_expr(_env, _assumptions, state, Expr::False, _places_live_on_exit) => (ScalarId::Bool, state)) |
ref| Line | Coverage | Source |
|---|---|---|
| 434 | ✗ | (borrow_check_place_expr( env, assumptions, state, place, ) => (place, state)) |
| 442 | N/A | (let access_kind = match kind { RefKind::Shared => AccessKind::Read, RefKind::Mut => AccessKind::Write, }) |
| 446 | 1 | (access_permitted( env, assumptions, state, Access::new(access_kind, place), places_live_on_exit, ) => state) |
| 455 | N/A | (let state = state.with_loan(Loan::new(lt, place, kind))) |
| 456 | N/A | (let ty = place.ty.ref_ty_of_kind(kind, lt)) |
| ──────── ("ref") | ||
| 458 | 17 | (borrow_check_expr(env, assumptions, state, Expr::Ref { kind, lt, place }, places_live_on_exit) => (ty, state)) |
place| Line | Coverage | Source |
|---|---|---|
| 462 | 2 | (borrow_check_place_expr(env, assumptions, state, place) => (place, state)) |
| 463 | ✗ | (access_kind_for_place_use(env, assumptions, state, place) => (access_kind, state)) |
| 464 | 11 | (access_permitted(env, assumptions, state, Access::new(access_kind, place), places_live_on_exit) => state) |
| 465 | N/A | (let state = if matches!(access_kind, AccessKind::Move) { state.with_uninit(&place.to_place_expression()) } else { state.clone() }) |
| 466 | 2 | (prove_place_is_movable(env, assumptions, state, place) => state) |
| ──────── ("place") | ||
| 468 | 56 | (borrow_check_expr(env, assumptions, state, Expr::Place(place), places_live_on_exit) => (&place.ty, state)) |
fn-name| Line | Coverage | Source |
|---|---|---|
| 474 | ✗ | (if let PlaceExpr::Var(id) = place) |
| 475 | ✗ | (if !state.has_local(id)) |
| 476 | 1 | (let fn_decl = env.crates().fn_named(id)?) |
| 477 | 1 | (if fn_decl.binder.len() == 0) |
| 478 | N/A | (let ty = Ty::rigid(RigidName::fn_def(id), ())) |
| ──────── ("fn-name") | ||
| 481 | 7 | (borrow_check_expr(env, _assumptions, state, Expr::Place(place), _places_live_on_exit) => (ty, state)) |
turbofish| Line | Coverage | Source |
|---|---|---|
| 486 | ✗ | (let fn_decl = env.crates().fn_named(id)?) |
| 487 | 1 | (if fn_decl.binder.len() == args.len()) |
| 488 | N/A | (let ty = Ty::rigid(RigidName::fn_def(id), args)) |
| ──────── ("turbofish") | ||
| 491 | 8 | (borrow_check_expr(env, _assumptions, state, Expr::Turbofish { id, args }, _places_live_on_exit) => (ty, state)) |
struct| Line | Coverage | Source |
|---|---|---|
| 511 | 1 | (let Struct { id: _, binder } = env.crates().struct_named(&adt_id)?) |
| 512 | ✗ | (if turbofish.parameters.len() == binder.len()) |
| 513 | ✗ | (let StructBoundData { where_clauses, fields } = binder.instantiate_with(&turbofish.parameters)?) |
| 516 | N/A | (let expected_names: Set<&FieldName> = fields.iter().map(|f| &f.name).collect()) |
| 517 | N/A | (let provided_names: Set<&FieldName> = field_exprs.iter().map(|fe| &fe.name).collect()) |
| 518 | ✗ | (if expected_names == provided_names) |
| 521 | ✗ | (for_all(i in 0..field_exprs.len()) with(state) (field in fields) (if field.name == field_exprs[i].name) (borrow_check_expr_has_ty(env, assumptions, state, &field_exprs[i].value, &field.ty, places_live_on_exit) => state)) |
| 526 | ✗ | (prove_where_clauses(env, assumptions, state, where_clauses) => state) |
| 528 | N/A | (let ty = RigidTy::new(adt_id, &turbofish.parameters)) |
| ──────── ("struct") | ||
| 530 | 7 | (borrow_check_expr(env, assumptions, state, Expr::Struct { adt_id, turbofish, field_exprs }, places_live_on_exit) => (ty, state)) |