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:54
- args
- for_all mod.rs:41
  - for_all mod.rs:51
    
    args
    
    check_crate (check crate) mod.rs:75
    
    args
    
    for_all mod.rs:60
    
    for_all mod.rs:72
    
    args
    
    check_crate_item (trait) mod.rs:188
    
    args
    
    check_trait (check trait) traits.rs:26
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    for_all traits.rs:9
    
    for_all traits.rs:24
    
    args
    
    check_trait_item (fn in trait) traits.rs:44
    
    args
    
    check_fn_in_trait (check fn in trait) traits.rs:68
    
    args
    
    check_fn (check fn) fns.rs:56
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    prove_wc_list (some) prove_wc_list.rs:28
    
    args
    
    prove_wc (parameter well formed) prove_wc.rs:160
    
    args
    
    prove_wf (tuples) prove_wf.rs:50
    
    args
    
    prove_after (prove_after) prove_after.rs:20
    
    args
    
    prove_wc_list (none) prove_wc_list.rs:21
    
    args
    
    check_fn_body (no fn body) fns.rs:76
    
    args
    
    check_coherence (check_coherence) coherence.rs:24
    
    args