Positive coverage: check_fn_body / no fn body
no fn body| Line | Coverage | Source |
|---|---|---|
| ──────── ("no fn body") | ||
| 77 | 1 | (check_fn_body(program, env, assumptions, MaybeFnBody::NoFnBody, input_args, output_ty) => ()) |
1 test exercised this rule:
Source location: tests/traits.rs:13
Proof tree
check_all_crates (check all prefixes)mod.rs:54for_allmod.rs:41for_allmod.rs:51check_crate (check crate)mod.rs:75for_allmod.rs:60for_allmod.rs:72check_crate_item (trait)mod.rs:173check_trait (check trait)traits.rs:26prove_wc_list (none)prove_wc_list.rs:24for_alltraits.rs:9for_alltraits.rs:24check_trait_item (fn in trait)traits.rs:44check_fn_in_trait (check fn in trait)traits.rs:68check_fn (check fn)fns.rs:56prove_wc_list (none)prove_wc_list.rs:24prove_wc_list (some)prove_wc_list.rs:31prove_wc (parameter well formed)prove_wc.rs:162prove_wf (tuples)prove_wf.rs:53
prove_after (prove_after)prove_after.rs:20prove_wc_list (none)prove_wc_list.rs:24
check_fn_body (no fn body)fns.rs:76
check_coherence (check_coherence)coherence.rs:24