Judgment borrow_check_statement at crates/formality-rust/src/check/borrow_check/nll.rs:176
Signature:
borrow_check_statement(env: TypeckEnv, assumptions: Wcs, state: FlowState, statement: Stmt, places_live_on_exit: LivePlaces,) => (TypeckEnv, FlowState)No applicable rule observed: at least one test exercised this judgment with no matching rule.
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.
let| Line | Coverage | Source |
|---|---|---|
| 188 | 1 | (prove_ty_is_wf(env, assumptions, state, ty) => state) |
| 191 | ✗ | (for_all(init in init.into_iter()) with (state) // FIXME: should make syntax for this (let Init { expr } = init) (borrow_check_expr_has_ty(env, assumptions, state, expr, ty, LiveBefore::live_before(&Assignment(id), env, &state, &places_live_on_exit), ) => state)) |
| 201 | ✗ | (let state = state.with_local_in_scope(&env.env, label, id, ty)?) |
| 202 | N/A | (let state = if init.is_none() { state.with_uninit(&PlaceExpr::Var(id.clone())) } else { state.with_initialized(&PlaceExpr::Var(id.clone())) }) |
| ──────── ("let") | ||
| 204 | 55 | (borrow_check_statement(env, assumptions, state, Stmt::Let { label, id, ty, init }, places_live_on_exit) => (env, state)) |
if| Line | Coverage | Source |
|---|---|---|
| 209 | ✗ | (borrow_check_expr_has_ty( env, assumptions, state, condition, Ty::bool(), Either(then_block, else_block).live_before(env, &state, places_live_on_exit), ) => state) |
| 219 | 1 | (borrow_check_block(env, assumptions, state, then_block, places_live_on_exit) => then_state) |
| 220 | 1 | (borrow_check_block(env, assumptions, state, else_block, places_live_on_exit) => else_state) |
| 223 | N/A | (let state: FlowState = Union((then_state, else_state)).upcast()) |
| ──────── ("if") | ||
| 225 | 14 | (borrow_check_statement(env, assumptions, state, Stmt::If { condition, then_block, else_block }, places_live_on_exit) => (env, state)) |
expr| Line | Coverage | Source |
|---|---|---|
| 229 | 12 | (borrow_check_expr( env, assumptions, state, expr, places_live_on_exit ) => (_init_ty, state)) |
| ──────── ("expr") | ||
| 237 | 15 | (borrow_check_statement(env, assumptions, state, Stmt::Expr { expr }, places_live_on_exit) => (env, state)) |
loop| Line | Coverage | Source |
|---|---|---|
| 244 | N/A | (let continue_live = Stmt::loop_(label, body).live_before(&env, &state, places_live_on_exit)) |
| 245 | ✗ | (let state = state.push_continue_scope(&env.env, label, places_live_on_exit, continue_live)?) |
| 246 | 6 | (borrow_check_loop(env, assumptions, state, body, places_live_on_exit) => state) |
| 247 | N/A | (let state = state.pop_scope(label)) |
| ──────── ("loop") | ||
| 249 | 13 | (borrow_check_statement(env, assumptions, state, Stmt::Loop { label, body }, places_live_on_exit) => (env, state)) |
break| Line | Coverage | Source |
|---|---|---|
| 255 | ✗ | (if state.scope_has_label(label)) |
| 256 | N/A | (let locals_to_drop = state.locals_dropped_to_label(label)) |
| 257 | 2 | (drop_places(env, assumptions, state, locals_to_drop, places_live_on_exit) => state) |
| 258 | N/A | (let state = state.with_break(label)) |
| 259 | N/A | (let state = state.diverges()) |
| ──────── ("break") | ||
| 261 | 11 | (borrow_check_statement(env, assumptions, state, Stmt::Break { label }, places_live_on_exit) => (env, state)) |
continue| Line | Coverage | Source |
|---|---|---|
| 267 | ✗ | (if state.scope_has_label(label)) |
| 268 | 1 | (if let Some(places_live_on_continue) = state.live_after_continue(label)) |
| 269 | N/A | (let locals_to_drop = state.locals_dropped_to_label(label)) |
| 270 | 1 | (drop_places(env, assumptions, state, locals_to_drop, places_live_on_continue) => state) |
| 271 | N/A | (let state = state.with_continue(label)) |
| 272 | N/A | (let state = state.diverges()) |
| ──────── ("continue") | ||
| 274 | 3 | (borrow_check_statement(env, assumptions, state, Stmt::Continue { label }, places_live_on_exit) => (env, state)) |
return| Line | Coverage | Source |
|---|---|---|
| 279 | 3 | (borrow_check_expr(env, assumptions, state, expr, LivePlaces::default()) => (expr_ty, state)) |
| 280 | ✗ | (if let Some(output_ty) = &env.output_ty) |
| 281 | 4 | (prove_assignable(env, assumptions, state, expr_ty, output_ty) => state) |
| 282 | N/A | (let state = state.diverges()) |
| ──────── ("return") | ||
| 284 | 49 | (borrow_check_statement(env, assumptions, state, Stmt::Return { expr }, _places_live_on_exit) => (env, state)) |
block| Line | Coverage | Source |
|---|---|---|
| 289 | 4 | (borrow_check_block(env, assumptions, state, block, places_live_on_exit) => state) |
| ──────── ("block") | ||
| 291 | 6 | (borrow_check_statement(env, assumptions, state, Stmt::Block(block), places_live_on_exit) => (env, state)) |
exists| Line | Coverage | Source |
|---|---|---|
| 296 | N/A | (let (env, subst, block) = env.instantiate_existentially(binder)) |
| 297 | N/A | (let assumptions_body = (assumptions, wf_assumptions_for_existential_subst(&subst))) |
| 298 | 19 | (borrow_check_block(env, assumptions_body, state, block, places_live_on_exit) => state) |
| 299 | N/A | (let state = state.pop_subst(&env.env, subst)) |
| ──────── ("exists") | ||
| 301 | 23 | (borrow_check_statement(env, assumptions, state, Stmt::Exists { binder }, places_live_on_exit) => (env, state)) |
print| Line | Coverage | Source |
|---|---|---|
| 306 | ✗ | (borrow_check_expr( env, assumptions, state, expr, places_live_on_exit ) => (_expr_ty, state)) |
| ──────── ("print") | ||
| 314 | 24 | (borrow_check_statement(env, assumptions, state, Stmt::Print { expr }, places_live_on_exit) => (env, state)) |