Judgment borrow_check_statement
judgment_fn! {
/// Prove that any loans issued in this statement are respected.
fn borrow_check_statement(
env: TypeckEnv,
assumptions: Predicates,
state: FlowState,
statement: Stmt,
places_live_on_exit: LivePlaces,
) => (TypeckEnv, FlowState) {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/borrow_check/nll.rs:174
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 |
|---|---|---|
| 186 | ✗ | (prove_ty_is_wf(env, assumptions, state, ty) => state) |
| 189 | 36 | (borrow_check_expr_has_ty(env, assumptions, state, expr, ty, LiveBefore::live_before(&Assignment(id), env, &state, &places_live_on_exit), ) => state) |
| 196 | ✗ | (let state = state.with_local_in_scope(&env.env, label, id, ty)?) |
| 197 | N/A | (let state = state.with_initialized(&PlaceExpr::Var(id.clone()))) |
| ──────── ("let") | ||
| 199 | 94 | (borrow_check_statement(env, assumptions, state, Stmt::Let { label, id, ty, init: Some(Init { expr }) }, places_live_on_exit) => (env, state)) |
let-no-init| Line | Coverage | Source |
|---|---|---|
| 203 | 1 | (prove_ty_is_wf(env, assumptions, state, ty) => state) |
| 204 | ✗ | (let state = state.with_local_in_scope(&env.env, label, id, ty)?) |
| 205 | N/A | (let state = state.with_uninit(&PlaceExpr::Var(id.clone()))) |
| ──────── ("let-no-init") | ||
| 207 | 6 | (borrow_check_statement(env, assumptions, state, Stmt::Let { label, id, ty, init: None }, places_live_on_exit) => (env, state)) |
if| Line | Coverage | Source |
|---|---|---|
| 212 | ✗ | (borrow_check_expr_has_ty( env, assumptions, state, condition, Ty::bool(), Either(then_block, &else_block.block).live_before(env, &state, places_live_on_exit), ) => state) |
| 222 | 2 | (borrow_check_block(env, assumptions, state, then_block, places_live_on_exit) => then_state) |
| 223 | 4 | (borrow_check_block(env, assumptions, state, &else_block.block, places_live_on_exit) => else_state) |
| 226 | N/A | (let state: FlowState = Union((then_state, else_state)).upcast()) |
| ──────── ("if") | ||
| 228 | 29 | (borrow_check_statement(env, assumptions, state, Stmt::If { condition, then_block, else_block }, places_live_on_exit) => (env, state)) |
expr| Line | Coverage | Source |
|---|---|---|
| 232 | 26 | (borrow_check_expr( env, assumptions, state, expr, places_live_on_exit ) => (_init_ty, state)) |
| ──────── ("expr") | ||
| 240 | 47 | (borrow_check_statement(env, assumptions, state, Stmt::Expr { expr }, places_live_on_exit) => (env, state)) |
loop| Line | Coverage | Source |
|---|---|---|
| 247 | N/A | (let continue_live = Stmt::loop_(label, body).live_before(&env, &state, places_live_on_exit)) |
| 248 | ✗ | (let state = state.push_continue_scope(&env.env, label, places_live_on_exit, continue_live)?) |
| 249 | 9 | (borrow_check_loop(env, assumptions, state, body, places_live_on_exit) => state) |
| 250 | N/A | (let state = state.pop_scope(label)) |
| ──────── ("loop") | ||
| 252 | 23 | (borrow_check_statement(env, assumptions, state, Stmt::Loop { label, body }, places_live_on_exit) => (env, state)) |
break| Line | Coverage | Source |
|---|---|---|
| 258 | ✗ | (if state.scope_has_label(label)) |
| 259 | N/A | (let locals_to_drop = state.locals_dropped_to_label(label)) |
| 260 | 2 | (drop_places(env, assumptions, state, locals_to_drop, places_live_on_exit) => state) |
| 261 | N/A | (let state = state.with_break(label)) |
| 262 | N/A | (let state = state.diverges()) |
| ──────── ("break") | ||
| 264 | 17 | (borrow_check_statement(env, assumptions, state, Stmt::Break { label }, places_live_on_exit) => (env, state)) |
continue| Line | Coverage | Source |
|---|---|---|
| 270 | ✗ | (if state.scope_has_label(label)) |
| 271 | 1 | (if let Some(places_live_on_continue) = state.live_after_continue(label)) |
| 272 | N/A | (let locals_to_drop = state.locals_dropped_to_label(label)) |
| 273 | 1 | (drop_places(env, assumptions, state, locals_to_drop, places_live_on_continue) => state) |
| 274 | N/A | (let state = state.with_continue(label)) |
| 275 | N/A | (let state = state.diverges()) |
| ──────── ("continue") | ||
| 277 | 3 | (borrow_check_statement(env, assumptions, state, Stmt::Continue { label }, places_live_on_exit) => (env, state)) |
return| Line | Coverage | Source |
|---|---|---|
| 282 | 5 | (borrow_check_expr(env, assumptions, state, expr, LivePlaces::default()) => (expr_ty, state)) |
| 283 | ✗ | (if let Some(output_ty) = &env.output_ty) |
| 284 | 4 | (prove_assignable(env, assumptions, state, expr_ty, output_ty) => state) |
| 285 | N/A | (let state = state.diverges()) |
| ──────── ("return") | ||
| 287 | 79 | (borrow_check_statement(env, assumptions, state, Stmt::Return { expr }, _places_live_on_exit) => (env, state)) |
block| Line | Coverage | Source |
|---|---|---|
| 292 | 4 | (borrow_check_block(env, assumptions, state, block, places_live_on_exit) => state) |
| ──────── ("block") | ||
| 294 | 6 | (borrow_check_statement(env, assumptions, state, Stmt::Block(block), places_live_on_exit) => (env, state)) |
exists| Line | Coverage | Source |
|---|---|---|
| 298 | ✗ | (if feature_gate_enabled_in_program(&env.program, &FeatureGateName::PoloniusUnlocked)) |
| 300 | ✗ | (scope(env.enter_existentially(&with_variables(binder)) => (env, (vars, block))) with(state) (let assumptions_body = (assumptions, wf_assumptions_for_existential_vars(vars))) (borrow_check_block(env, assumptions_body, state, block, places_live_on_exit) => state)) |
| ──────── ("exists") | ||
| 304 | 48 | (borrow_check_statement(env, assumptions, state, Stmt::Exists { binder }, places_live_on_exit) => (env, state)) |
exists| Line | Coverage | Source |
|---|---|---|
| 308 | ✗ | (if feature_gate_enabled_in_program(&env.program, &FeatureGateName::PoloniusAlpha)) |
| 310 | ✗ | (scope(env.enter_existentially(&with_variables(binder)) => (env, (vars, block))) with(state) (let assumptions_body = (assumptions, wf_assumptions_for_existential_vars(vars))) (borrow_check_block(env, assumptions_body, state, block, places_live_on_exit) => state) // Although we do not rerun borrowck with all outlives, Polonius Alpha // does not change universal region constraints being checked on the // full outlives set. (verify_universal_outlives(env, assumptions_body, &state.all_outlives) => ())) |
| ──────── ("exists") | ||
| 318 | 48 | (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 | ✗ | (scope(env.enter_existentially(&with_variables(binder)) => (env, (vars, block))) with(state) (let assumptions_body = (assumptions, wf_assumptions_for_existential_vars(vars))) (let entry_state = state.clone()) (borrow_check_block(env, assumptions_body, state, block, places_live_on_exit) => state) // Rerun borrowck again, with the *entry* state combined with the entire outlives set. (let state = entry_state.with_global_outlives_from(&state)) (borrow_check_block(env, assumptions_body, state, block, places_live_on_exit) => state)) |
| ──────── ("exists") | ||
| 332 | 48 | (borrow_check_statement(env, assumptions, state, Stmt::Exists { binder }, places_live_on_exit) => (env, state)) |
print| Line | Coverage | Source |
|---|---|---|
| 337 | ✗ | (borrow_check_expr( env, assumptions, state, expr, places_live_on_exit ) => (_expr_ty, state)) |
| ──────── ("print") | ||
| 345 | 75 | (borrow_check_statement(env, assumptions, state, Stmt::Print { expr }, places_live_on_exit) => (env, state)) |