diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-04-28 15:35:43 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-04-28 15:35:43 +0200 |
| commit | 2fbdb0c45f0913b9fd8e95606c525fc5bfb3bc6d (patch) | |
| tree | e0da01bfc65fd80c2742816892f4e48843d959c3 /exportclight | |
| parent | befe864384244c47f42d891068aba6f14287ff8e (diff) | |
| download | compcert-kvx-2fbdb0c45f0913b9fd8e95606c525fc5bfb3bc6d.tar.gz compcert-kvx-2fbdb0c45f0913b9fd8e95606c525fc5bfb3bc6d.zip | |
Issue #179: clightgen produces wrong abstract syntax for "switch" statements
Diffstat (limited to 'exportclight')
| -rw-r--r-- | exportclight/ExportClight.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 003e97ee..8001dca7 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -124,6 +124,11 @@ let coqsingle p n = let coqN p n = fprintf p "%ld%%N" (N.to_int32 n) +let coqZ p n = + if Z.ge n Z.zero + then fprintf p "%s" (Z.to_string n) + else fprintf p "(%s)" (Z.to_string n) + (* Coq strings *) let coqstring p s = @@ -364,10 +369,10 @@ let rec stmt p = function and lblstmts p = function | LSnil -> - () + (fprintf p "LSnil") | LScons(lbl, s, ls) -> - fprintf p "@[<hv 2>(LScase %a@ %a@ %a)@]" - (print_option coqint) lbl stmt s lblstmts ls + fprintf p "@[<hv 2>(LScons %a@ %a@ %a)@]" + (print_option coqZ) lbl stmt s lblstmts ls let print_function p (id, f) = fprintf p "Definition f_%s := {|@ " (extern_atom id); |