Judgment borrow_check_statement at crates/formality-rust/src/check/borrow_check/nll.rs:177
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 |
|---|---|---|
| 189 | 1 | (prove_ty_is_wf(env, assumptions, state, ty) => state) |
| 192 | ✗ | (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)) |
| 202 | ✗ | (let state = state.with_local_in_scope(&env.env, label, id, ty)?) |
| 203 | N/A | (let state = if init.is_none() { state.with_uninit(&PlaceExpr::Var(id.clone())) } else { state.with_initialized(&PlaceExpr::Var(id.clone())) }) |
| ──────── ("let") | ||
| 205 | 87 | (borrow_check_statement(env, assumptions, state, Stmt::Let { label, id, ty, init }, places_live_on_exit) => (env, state)) |
if| Line | Coverage | Source |
|---|---|---|
| 210 | ✗ | (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) |
| 220 | 2 | (borrow_check_block(env, assumptions, state, then_block, places_live_on_exit) => then_state) |
| 221 | 3 | (borrow_check_block(env, assumptions, state, else_block, places_live_on_exit) => else_state) |
| 224 | N/A | (let state: FlowState = Union((then_state, else_state)).upcast()) |
| ──────── ("if") | ||
| 226 | 45 | (borrow_check_statement(env, assumptions, state, Stmt::If { condition, then_block, else_block }, places_live_on_exit) => (env, state)) |
expr| Line | Coverage | Source |
|---|---|---|
| 230 | 18 | (borrow_check_expr( env, assumptions, state, expr, places_live_on_exit ) => (_init_ty, state)) |
| ──────── ("expr") | ||
| 238 | 36 | (borrow_check_statement(env, assumptions, state, Stmt::Expr { expr }, places_live_on_exit) => (env, state)) |
loop| Line | Coverage | Source |
|---|---|---|
| 245 | N/A | (let continue_live = Stmt::loop_(label, body).live_before(&env, &state, places_live_on_exit)) |
| 246 | ✗ | (let state = state.push_continue_scope(&env.env, label, places_live_on_exit, continue_live)?) |
| 247 | 10 | (borrow_check_loop(env, assumptions, state, body, places_live_on_exit) => state) |
| 248 | N/A | (let state = state.pop_scope(label)) |
| ──────── ("loop") | ||
| 250 | 34 | (borrow_check_statement(env, assumptions, state, Stmt::Loop { label, body }, places_live_on_exit) => (env, state)) |
break| Line | Coverage | Source |
|---|---|---|
| 256 | ✗ | (if state.scope_has_label(label)) |
| 257 | N/A | (let locals_to_drop = state.locals_dropped_to_label(label)) |
| 258 | 2 | (drop_places(env, assumptions, state, locals_to_drop, places_live_on_exit) => state) |
| 259 | N/A | (let state = state.with_break(label)) |
| 260 | N/A | (let state = state.diverges()) |
| ──────── ("break") | ||
| 262 | 24 | (borrow_check_statement(env, assumptions, state, Stmt::Break { label }, places_live_on_exit) => (env, state)) |
continue| Line | Coverage | Source |
|---|---|---|
| 268 | ✗ | (if state.scope_has_label(label)) |
| 269 | 1 | (if let Some(places_live_on_continue) = state.live_after_continue(label)) |
| 270 | N/A | (let locals_to_drop = state.locals_dropped_to_label(label)) |
| 271 | 1 | (drop_places(env, assumptions, state, locals_to_drop, places_live_on_continue) => state) |
| 272 | N/A | (let state = state.with_continue(label)) |
| 273 | N/A | (let state = state.diverges()) |
| ──────── ("continue") | ||
| 275 | 3 | (borrow_check_statement(env, assumptions, state, Stmt::Continue { label }, places_live_on_exit) => (env, state)) |
return| Line | Coverage | Source |
|---|---|---|
| 280 | 4 | (borrow_check_expr(env, assumptions, state, expr, LivePlaces::default()) => (expr_ty, state)) |
| 281 | ✗ | (if let Some(output_ty) = &env.output_ty) |
| 282 | 4 | (prove_assignable(env, assumptions, state, expr_ty, output_ty) => state) |
| 283 | N/A | (let state = state.diverges()) |
| ──────── ("return") | ||
| 285 | 81 | (borrow_check_statement(env, assumptions, state, Stmt::Return { expr }, _places_live_on_exit) => (env, state)) |
block| Line | Coverage | Source |
|---|---|---|
| 290 | 4 | (borrow_check_block(env, assumptions, state, block, places_live_on_exit) => state) |
| ──────── ("block") | ||
| 292 | 6 | (borrow_check_statement(env, assumptions, state, Stmt::Block(block), places_live_on_exit) => (env, state)) |
exists| Line | Coverage | Source |
|---|---|---|
| 296 | ✗ | (if feature_gate_enabled_in_program(&env.program, &FeatureGateName::PoloniusUnlocked)) |
| 298 | N/A | (let (env, subst, block) = env.instantiate_existentially(binder)) |
| 299 | N/A | (let assumptions_body = (assumptions, wf_assumptions_for_existential_subst(&subst))) |
| 300 | 1 | (borrow_check_block(env, assumptions_body, state, block, places_live_on_exit) => state) |
| 301 | N/A | (let state = state.pop_subst(&env.env, subst)) |
| ──────── ("exists") | ||
| 303 | 54 | (borrow_check_statement(env, assumptions, state, Stmt::Exists { binder }, places_live_on_exit) => (env, state)) |
exists| Line | Coverage | Source |
|---|---|---|
| 307 | ✗ | (if feature_gate_enabled_in_program(&env.program, &FeatureGateName::PoloniusAlpha)) |
| 309 | N/A | (let (env, subst, block) = env.instantiate_existentially(binder)) |
| 310 | N/A | (let assumptions_body = (assumptions, wf_assumptions_for_existential_subst(&subst))) |
| 311 | 3 | (borrow_check_block(env, assumptions_body, state, block, places_live_on_exit) => state) |
| 315 | 1 | (verify_universal_outlives(env, assumptions_body, &state.all_outlives) => ()) |
| 316 | N/A | (let state = state.pop_subst(&env.env, subst)) |
| ──────── ("exists") | ||
| 318 | 54 | (borrow_check_statement(env, assumptions, state, Stmt::Exists { binder }, places_live_on_exit) => (env, state)) |
exists| Line | Coverage | Source |
|---|---|---|
| 322 | ✗ | (if !feature_gate_enabled_in_program(&env.program, &FeatureGateName::PoloniusUnlocked) && !feature_gate_enabled_in_program(&env.program, &FeatureGateName::PoloniusAlpha)) |
| 324 | N/A | (let (env, subst, block) = env.instantiate_existentially(binder)) |
| 325 | N/A | (let assumptions_body = (assumptions, wf_assumptions_for_existential_subst(&subst))) |
| 326 | N/A | (let entry_state = state.clone()) |
| 327 | 23 | (borrow_check_block(env, assumptions_body, state, block, places_live_on_exit) => state) |
| 329 | N/A | (let state = entry_state.with_global_outlives_from(&state)) |
| 330 | 6 | (borrow_check_block(env, assumptions_body, state, block, places_live_on_exit) => state) |
| 331 | N/A | (let state = state.pop_subst(&env.env, subst)) |
| ──────── ("exists") | ||
| 333 | 54 | (borrow_check_statement(env, assumptions, state, Stmt::Exists { binder }, places_live_on_exit) => (env, state)) |
print| Line | Coverage | Source |
|---|---|---|
| 338 | ✗ | (borrow_check_expr( env, assumptions, state, expr, places_live_on_exit ) => (_expr_ty, state)) |
| ──────── ("print") | ||
| 346 | 24 | (borrow_check_statement(env, assumptions, state, Stmt::Print { expr }, places_live_on_exit) => (env, state)) |