judgment_fn! {
/// Check the function body, dispatching to the borrow checker for expression bodies.
fn check_fn_body(
program: Program,
env: Env,
assumptions: Predicates,
body: MaybeFnBody,
input_args: Vec<crate::grammar::InputArg>,
output_ty: crate::grammar::Ty,
) => () {
/* rules omitted */
}
}
Source: crates/formality-rust/src/check/fns.rs:61
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.
no fn body
| Line | Coverage | Source |
|---|
| | ──────── ("no fn body") |
| 76 | 192 | (check_fn_body(program, env, assumptions, MaybeFnBody::NoFnBody, input_args, output_ty) => ()) |
trusted fn body
| Line | Coverage | Source |
|---|
| | ──────── ("trusted fn body") |
| 82 | 15 | (check_fn_body(program, env, assumptions, MaybeFnBody::FnBody(FnBody::TrustedFnBody), input_args, output_ty) => ()) |
expr fn body
| Line | Coverage | Source |
|---|
| 87 | N/A | (let typeck_env = TypeckEnv::for_fn_body(env, program, output_ty)) |
| 88 | ✗ | (let initial_state = FlowState::for_fn_body(env, input_args)?) |
| 89 | 79 | (borrow_check(typeck_env, assumptions, initial_state, block) => ()) |
| | ──────── ("expr fn body") |
| 91 | 175 | (check_fn_body(program, env, assumptions, MaybeFnBody::FnBody(FnBody::Expr(block)), input_args, output_ty) => ()) |
How to read this page