diff options
| -rw-r--r-- | Changelog | 3 | ||||
| -rw-r--r-- | exportclight/ExportClight.ml | 11 |
2 files changed, 11 insertions, 3 deletions
@@ -1,5 +1,8 @@ - Removed the compilation of '.cm' files written in Cminor concrete syntax. +Bug fixing: +- Issue #179: clightgen produces wrong output for "switch" statements. + Release 3.0.1, 2017-02-14 ========================= 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); |