diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index 12a5a4f9b..127a344ca 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -767,7 +767,7 @@ module Make (C : CONFIG) = struct (* Get the number of cases, because we don't want to check branch coverage for matches with only a single case. *) let num_cases = List.length cases in - let branch_id, on_reached = coverage_branch_reached ctx l in + let branch_id, on_reached = if num_cases > 1 then coverage_branch_reached ctx l else (0, []) in let case_return_id = ngensym () in let finish_match_label = label "finish_match_" in let compile_case (apat, guard, body) = @@ -807,7 +807,7 @@ module Make (C : CONFIG) = struct in ( aval_setup @ [icomment ("Case with num_cases: " ^ string_of_int num_cases)] - @ (if num_cases > 1 then on_reached else []) + @ on_reached @ [idecl l ctyp case_return_id] @ List.concat (List.map compile_case cases) @ [imatch_failure l] diff --git a/test/sailcov/let_single_branch.expect b/test/sailcov/let_single_branch.expect new file mode 100644 index 000000000..e8e533070 --- /dev/null +++ b/test/sailcov/let_single_branch.expect @@ -0,0 +1,25 @@ + + +
+ +
+default Order dec
+$include <prelude.sail>
+
+register R : bool = true
+val main : unit -> unit
+
+function main() = {
+ let (x, y) = (R, R);
+ if x then {
+ print_endline("A")
+ } else {
+ print_endline("B")
+ }
+}
+
+
+
\ No newline at end of file
diff --git a/test/sailcov/let_single_branch.sail b/test/sailcov/let_single_branch.sail
new file mode 100644
index 000000000..f734ed5d2
--- /dev/null
+++ b/test/sailcov/let_single_branch.sail
@@ -0,0 +1,14 @@
+default Order dec
+$include