diff options
| author | Brian Campbell | 2020-11-18 11:04:12 +0000 |
|---|---|---|
| committer | Brian Campbell | 2020-11-18 11:04:12 +0000 |
| commit | 6198232aef876842be8be3641be7faf0cad5b4a5 (patch) | |
| tree | 225f6e64cd5a2f7a42908a3a2834ace18b7be7ec /src/jib | |
| parent | f19dfa41af10343aafcaa21f5a764a7a56a64bcb (diff) | |
Fix coverage information in case branches that immediately return
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/jib_compile.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index cd4edd12..fb86333f 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -720,8 +720,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup @ [iif l (V_call (Bnot, [V_id (gs, CT_bool)])) (destructure_cleanup @ [igoto case_label]) [] CT_unit] else []) - @ body_setup @ (if num_cases > 1 then coverage_branch_taken branch_id body else []) + @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup @ [igoto finish_match_label] in |