From 1cd385f3b354a78ae8d02333f40cd065073c9b19 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 21 Dec 2013 17:00:43 +0000
Subject: Support "default" cases in the middle of a "switch", not just at the
 end.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2383 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/PrintCsyntax.ml | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

(limited to 'cfrontend/PrintCsyntax.ml')

diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index fc60f335..4db89761 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -324,20 +324,22 @@ let rec print_stmt p s =
 
 and print_cases p cases =
   match cases with
-  | LSdefault Sskip ->
+  | LSnil ->
       ()
-  | LSdefault s ->
-      fprintf p "@[<v 2>default:@ %a@]" print_stmt s
-  | LScase(lbl, Sskip, rem) ->
-      fprintf p "case %ld:@ %a"
-              (camlint_of_coqint lbl)
+  | LScons(lbl, Sskip, rem) ->
+      fprintf p "%a:@ %a"
+              print_case_label lbl
               print_cases rem
-  | LScase(lbl, s, rem) ->
-      fprintf p "@[<v 2>case %ld:@ %a@]@ %a"
-              (camlint_of_coqint lbl)
+  | LScons(lbl, s, rem) ->
+      fprintf p "@[<v 2>%a:@ %a@]@ %a"
+              print_case_label lbl
               print_stmt s
               print_cases rem
 
+and print_case_label p = function
+  | None -> fprintf p "default"
+  | Some lbl -> fprintf p "case %ld" (camlint_of_coqint lbl)
+
 and print_stmt_for p s =
   match s with
   | Sskip ->
@@ -539,8 +541,8 @@ let rec collect_stmt = function
   | Sgoto lbl -> ()
 
 and collect_cases = function
-  | LSdefault s -> collect_stmt s
-  | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem
+  | LSnil -> ()
+  | LScons(lbl, s, rem) -> collect_stmt s; collect_cases rem
 
 let collect_function f =
   collect_type f.fn_return;
-- 
cgit