Judgment borrow_check_block
judgment_fn! {
/// Prove that any loans issued in this basic block are respected.
fn borrow_check_block(
env: TypeckEnv,
assumptions: Predicates,
state: FlowState,
block: Block,
places_live_on_exit: LivePlaces,
) => FlowState {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/borrow_check/nll.rs:142
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.
basic block| Line | Coverage | Source |
|---|---|---|
| 155 | ✗ | (let state = state.push_scope(&env.env, label, places_live_on_exit)?) |
| 156 | ✗ | (for_all(i in 0..stmts.len()) with(env, state) (borrow_check_statement( env, assumptions, state, &stmts[i], stmts[i+1..].live_before(env, &state, places_live_on_exit), ) => (env, state))) |
| 165 | N/A | (let locals_to_drop = state.locals_dropped_in_innermost_scope()) |
| 166 | 2 | (drop_places(env, assumptions, state, locals_to_drop, places_live_on_exit) => state) |
| 167 | N/A | (let state = state.pop_scope(label)) |
| ──────── ("basic block") | ||
| 169 | 175 | (borrow_check_block(env, assumptions, state, Block { label, stmts }, places_live_on_exit) => state) |