diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-21 17:00:43 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-21 17:00:43 +0000 |
commit | 1cd385f3b354a78ae8d02333f40cd065073c9b19 (patch) | |
tree | 923e490d77d414280d91918bcf5c35b93df78ab0 /cfrontend/PrintCsyntax.ml | |
parent | 1c768ee3ff91e826f52cf08e1aaa8c4d637240f5 (diff) |
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
Diffstat (limited to 'cfrontend/PrintCsyntax.ml')
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index fc60f33..4db8976 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; |